Theorem mpd3an3 1470

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

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

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

This theorem is referenced by:  stoic2b  1782  elovmpo  7608  f1oeng  8914  php  9138  nnsdomg  9206  wdomimag  9499  gruuni  10721  genpv  10920  pncan3  11399  mulsubaddmulsub  11612  infssuzle  12879  fzrevral3  13566  flflp1  13764  subsq2  14171  brfi1ind  14469  opfi1ind  14472  ccatws1ls  14594  swrdrlen  14620  pfxpfxid  14669  pfxcctswrd  14670  2cshwid  14774  caubnd  15319  dvdsmul1  16244  dvdsmul2  16245  hashbcval  16971  setsvalg  17134  ressval  17201  restval  17387  mrelatglb0  18525  imasmnd2  18740  efmndov  18847  qusinv  19163  ghminv  19196  gsmsymgrfixlem1  19400  gsmsymgreqlem2  19404  gexod  19559  lsmvalx  19612  rngrz  20145  imasring  20308  irredneg  20408  01eq0ring  20509  ocvin  21656  frlmiscvec  21831  evlrhm  22084  gsumsmonply1  22300  mat1mhm  22474  marrepfval  22550  marrepval0  22551  marepvfval  22555  marepvval0  22556  1elcpmat  22705  m2cpminv0  22751  idpm2idmp  22791  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  restin  23156  qtopval  23685  elqtop3  23693  elfm3  23940  flimval  23953  nmge0  24607  nmeq0  24608  nminv  24611  nmo0  24725  0nghm  24731  coemulhi  26244  isosctrlem2  26808  divsqrtsumlem  26968  2lgsoddprmlem4  27403  0uhgrrusgr  29672  frgruhgr0v  30359  nvge0  30769  nvnd  30784  dip0r  30813  dip0l  30814  nmoo0  30887  hi2eq  31201  wrdsplex  33022  resvval  33419  unitdivcld  34092  signspval  34743  satfv0  35593  ltflcei  37982  elghomlem1OLD  38259  rngorz  38297  rngonegmn1l  38315  rngonegmn1r  38316  igenval  38435  xrnidresex  38804  xrncnvepresex  38805  lfl0  39564  olj01  39724  olm11  39726  hl2at  39904  pmapeq0  40265  trlcl  40663  trlle  40683  tendoid  41272  tendo0plr  41291  tendoipl2  41297  erngmul  41305  erngmul-rN  41313  dvamulr  41511  dvavadd  41514  dvhmulr  41585  cdlemm10N  41617  repncan3  42867  pellfund14  43350  mendmulr  43636  onnoxpg  43880  fmuldfeq  46035  stoweidlem19  46469  stoweidlem26  46476  addsubeq0  47766  zp1modne  47822  modm1nep1  47841  prelspr  47968  lincval1  48917