Theorem mpd3an3 1492

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 700	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  stoic2b  1808  elovmpo  7693  f1oeng  9028  php  9253  nnsdomg  9322  wdomimag  9611  gruuni  10915  genpv  11114  pncan3  11595  mulsubaddmulsub  11810  infssuzle  13088  fzrevral3  13778  flflp1  13977  subsq2  14385  brfi1ind  14684  opfi1ind  14687  ccatws1ls  14812  swrdrlen  14840  pfxpfxid  14889  pfxcctswrd  14890  2cshwid  14996  caubnd  15558  dvdsmul1  16479  dvdsmul2  16480  hashbcval  17212  setsvalg  17376  ressval  17443  restval  17629  mrelatglb0  18767  imasmgm2  18895  imasmnd2  19000  efmndov  19109  qusinv  19437  ghminv  19469  gsmsymgrfixlem1  19674  gsmsymgreqlem2  19678  gexod  19833  lsmvalx  19886  rngrz  20421  imasring  20593  irredneg  20693  01eq0ring  20814  ocvin  22013  frlmiscvec  22188  evlrhm  22443  gsumsmonply1  22658  mat1mhm  22832  marrepfval  22908  marrepval0  22909  marepvfval  22913  marepvval0  22914  1elcpmat  23066  m2cpminv0  23112  idpm2idmp  23152  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  restin  23517  qtopval  24047  elqtop3  24055  elfm3  24302  flimval  24315  nmge0  24969  nmeq0  24970  nminv  24973  nmo0  25087  0nghm  25093  coemulhi  26606  isosctrlem2  27180  divsqrtsumlem  27340  2lgsoddprmlem4  27775  0uhgrrusgr  30192  frgruhgr0v  30898  nvge0  31308  nvnd  31323  dip0r  31352  dip0l  31353  nmoo0  31426  hi2eq  31740  wrdsplex  33576  resvval  33974  unitdivcld  34616  signspval  35264  satfv0  36303  ltflcei  38736  elghomlem1OLD  39022  rngorz  39060  rngonegmn1l  39078  rngonegmn1r  39079  igenval  39198  xrnidresex  39565  xrncnvepresex  39566  lfl0  40325  olj01  40485  olm11  40487  hl2at  40665  pmapeq0  41026  trlcl  41424  trlle  41444  tendoid  42033  tendo0plr  42052  tendoipl2  42058  erngmul  42066  erngmul-rN  42074  dvamulr  42272  dvavadd  42275  dvhmulr  42346  cdlemm10N  42378  repncan3  43638  pellfund14  44109  mendmulr  44389  onnoxpg  44633  fmuldfeq  46810  stoweidlem19  47244  stoweidlem26  47251  addsubeq0  48581  zp1modne  48637  modm1nep1  48656  prelspr  48783  lincval1  49746