Theorem mpd3an3 1491

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  stoic2b  1805  elovmpo  7657  f1oeng  8968  php  9192  nnsdomg  9260  wdomimag  9550  gruuni  10786  genpv  10985  pncan3  11466  mulsubaddmulsub  11679  infssuzle  12956  fzrevral3  13644  flflp1  13842  subsq2  14249  brfi1ind  14548  opfi1ind  14551  ccatws1ls  14673  swrdrlen  14699  pfxpfxid  14748  pfxcctswrd  14749  2cshwid  14853  caubnd  15412  dvdsmul1  16336  dvdsmul2  16337  hashbcval  17063  setsvalg  17227  ressval  17294  restval  17480  mrelatglb0  18618  imasmnd2  18833  efmndov  18941  qusinv  19262  ghminv  19294  gsmsymgrfixlem1  19498  gsmsymgreqlem2  19502  gexod  19657  lsmvalx  19710  rngrz  20245  imasring  20413  irredneg  20513  01eq0ring  20615  ocvin  21805  frlmiscvec  21980  evlrhm  22233  gsumsmonply1  22448  mat1mhm  22622  marrepfval  22698  marrepval0  22699  marepvfval  22703  marepvval0  22704  1elcpmat  22853  m2cpminv0  22899  idpm2idmp  22939  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  restin  23304  qtopval  23833  elqtop3  23841  elfm3  24088  flimval  24101  nmge0  24755  nmeq0  24756  nminv  24759  nmo0  24873  0nghm  24879  coemulhi  26392  isosctrlem2  26965  divsqrtsumlem  27125  2lgsoddprmlem4  27560  0uhgrrusgr  29909  frgruhgr0v  30596  nvge0  31006  nvnd  31021  dip0r  31050  dip0l  31051  nmoo0  31124  hi2eq  31438  wrdsplex  33237  resvval  33630  unitdivcld  34272  signspval  34920  satfv0  35831  ltflcei  38240  elghomlem1OLD  38517  rngorz  38555  rngonegmn1l  38573  rngonegmn1r  38574  igenval  38693  xrnidresex  39060  xrncnvepresex  39061  lfl0  39820  olj01  39980  olm11  39982  hl2at  40160  pmapeq0  40521  trlcl  40919  trlle  40939  tendoid  41528  tendo0plr  41547  tendoipl2  41553  erngmul  41561  erngmul-rN  41569  dvamulr  41767  dvavadd  41770  dvhmulr  41841  cdlemm10N  41873  repncan3  43125  pellfund14  43608  mendmulr  43894  onnoxpg  44138  fmuldfeq  46282  stoweidlem19  46716  stoweidlem26  46723  addsubeq0  48016  zp1modne  48072  modm1nep1  48091  prelspr  48218  lincval1  49182