Theorem mpd3an3 1461

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 1117	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 684	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  stoic2b  1778  elovmpo  7523  f1oeng  8768  php  9002  wdomimag  9355  gruuni  10565  genpv  10764  pncan3  11238  mulsubaddmulsub  11448  infssuzle  12680  fzrevral3  13352  flflp1  13536  subsq2  13936  brfi1ind  14222  opfi1ind  14225  ccatws1ls  14352  swrdrlen  14381  pfxpfxid  14431  pfxcctswrd  14432  2cshwid  14536  caubnd  15079  dvdsmul1  15996  dvdsmul2  15997  hashbcval  16712  setsvalg  16876  ressval  16953  restval  17146  mrelatglb0  18288  imasmnd2  18431  efmndov  18529  qusinv  18824  ghminv  18850  gsmsymgrfixlem1  19044  gsmsymgreqlem2  19048  gexod  19200  lsmvalx  19253  ringrz  19836  imasring  19867  irredneg  19961  ocvin  20888  frlmiscvec  21065  evlrhm  21315  gsumsmonply1  21483  mat1mhm  21642  marrepfval  21718  marrepval0  21719  marepvfval  21723  marepvval0  21724  1elcpmat  21873  m2cpminv0  21919  idpm2idmp  21959  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  restin  22326  qtopval  22855  elqtop3  22863  elfm3  23110  flimval  23123  nmge0  23782  nmeq0  23783  nminv  23786  nmo0  23908  0nghm  23914  coemulhi  25424  isosctrlem2  25978  divsqrtsumlem  26138  2lgsoddprmlem4  26572  0uhgrrusgr  27954  frgruhgr0v  28637  nvge0  29044  nvnd  29059  dip0r  29088  dip0l  29089  nmoo0  29162  hi2eq  29476  wrdsplex  31221  resvval  31535  unitdivcld  31860  signspval  32540  satfv0  33329  ltflcei  35774  elghomlem1OLD  36052  rngorz  36090  rngonegmn1l  36108  rngonegmn1r  36109  igenval  36228  xrnidresex  36540  xrncnvepresex  36541  lfl0  37086  olj01  37246  olm11  37248  hl2at  37426  pmapeq0  37787  trlcl  38185  trlle  38205  tendoid  38794  tendo0plr  38813  tendoipl2  38819  erngmul  38827  erngmul-rN  38835  dvamulr  39033  dvavadd  39036  dvhmulr  39107  cdlemm10N  39139  repncan3  40373  pellfund14  40727  mendmulr  41020  fmuldfeq  43131  stoweidlem19  43567  stoweidlem26  43574  addsubeq0  44799  prelspr  44949  lincval1  45771