Theorem mpd3an3 1459

Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)

Hypotheses

Ref	Expression
mpd3an3.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
mpd3an3.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpd3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		mpd3an3.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1116	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 686	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  stoic2b  1770  elovmpo  7660  f1oeng  8985  php  9228  nnsdomg  9320  wdomimag  9604  gruuni  10817  genpv  11016  pncan3  11492  mulsubaddmulsub  11702  infssuzle  12939  fzrevral3  13614  flflp1  13798  subsq2  14200  brfi1ind  14486  opfi1ind  14489  ccatws1ls  14609  swrdrlen  14635  pfxpfxid  14685  pfxcctswrd  14686  2cshwid  14790  caubnd  15331  dvdsmul1  16248  dvdsmul2  16249  hashbcval  16964  setsvalg  17128  ressval  17205  restval  17401  mrelatglb0  18546  imasmnd2  18724  efmndov  18826  qusinv  19138  ghminv  19170  gsmsymgrfixlem1  19375  gsmsymgreqlem2  19379  gexod  19534  lsmvalx  19587  rngrz  20099  imasring  20259  irredneg  20362  01eq0ring  20460  ocvin  21599  frlmiscvec  21776  evlrhm  22035  gsumsmonply1  22219  mat1mhm  22379  marrepfval  22455  marrepval0  22456  marepvfval  22460  marepvval0  22461  1elcpmat  22610  m2cpminv0  22656  idpm2idmp  22696  chfacfscmulgsum  22755  chfacfpmmulgsum  22759  restin  23063  qtopval  23592  elqtop3  23600  elfm3  23847  flimval  23860  nmge0  24519  nmeq0  24520  nminv  24523  nmo0  24645  0nghm  24651  coemulhi  26181  isosctrlem2  26744  divsqrtsumlem  26905  2lgsoddprmlem4  27341  0uhgrrusgr  29385  frgruhgr0v  30067  nvge0  30476  nvnd  30491  dip0r  30520  dip0l  30521  nmoo0  30594  hi2eq  30908  wrdsplex  32655  resvval  33032  unitdivcld  33496  signspval  34178  satfv0  34962  ltflcei  37075  elghomlem1OLD  37352  rngorz  37390  rngonegmn1l  37408  rngonegmn1r  37409  igenval  37528  xrnidresex  37873  xrncnvepresex  37874  lfl0  38531  olj01  38691  olm11  38693  hl2at  38872  pmapeq0  39233  trlcl  39631  trlle  39651  tendoid  40240  tendo0plr  40259  tendoipl2  40265  erngmul  40273  erngmul-rN  40281  dvamulr  40479  dvavadd  40482  dvhmulr  40553  cdlemm10N  40585  repncan3  41932  pellfund14  42312  mendmulr  42606  onnog  42853  fmuldfeq  44965  stoweidlem19  45401  stoweidlem26  45408  addsubeq0  46670  prelspr  46820  lincval1  47481

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »