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 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  7668  f1oeng  8976  php  9201  nnsdomg  9269  wdomimag  9559  gruuni  10803  genpv  11002  pncan3  11483  mulsubaddmulsub  11696  infssuzle  12973  fzrevral3  13661  flflp1  13860  subsq2  14267  brfi1ind  14566  opfi1ind  14569  ccatws1ls  14693  swrdrlen  14721  pfxpfxid  14770  pfxcctswrd  14771  2cshwid  14877  caubnd  15436  dvdsmul1  16360  dvdsmul2  16361  hashbcval  17087  setsvalg  17251  ressval  17318  restval  17504  mrelatglb0  18642  imasmnd2  18863  efmndov  18971  qusinv  19292  ghminv  19324  gsmsymgrfixlem1  19528  gsmsymgreqlem2  19532  gexod  19687  lsmvalx  19740  rngrz  20275  imasring  20445  irredneg  20545  01eq0ring  20665  ocvin  21861  frlmiscvec  22036  evlrhm  22289  gsumsmonply1  22504  mat1mhm  22678  marrepfval  22754  marrepval0  22755  marepvfval  22759  marepvval0  22760  1elcpmat  22909  m2cpminv0  22955  idpm2idmp  22995  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  restin  23360  qtopval  23889  elqtop3  23897  elfm3  24144  flimval  24157  nmge0  24811  nmeq0  24812  nminv  24815  nmo0  24929  0nghm  24935  coemulhi  26448  isosctrlem2  27021  divsqrtsumlem  27181  2lgsoddprmlem4  27616  0uhgrrusgr  29965  frgruhgr0v  30652  nvge0  31062  nvnd  31077  dip0r  31106  dip0l  31107  nmoo0  31180  hi2eq  31494  wrdsplex  33293  resvval  33680  unitdivcld  34322  signspval  34971  satfv0  35871  ltflcei  38300  elghomlem1OLD  38577  rngorz  38615  rngonegmn1l  38633  rngonegmn1r  38634  igenval  38753  xrnidresex  39120  xrncnvepresex  39121  lfl0  39880  olj01  40040  olm11  40042  hl2at  40220  pmapeq0  40581  trlcl  40979  trlle  40999  tendoid  41588  tendo0plr  41607  tendoipl2  41613  erngmul  41621  erngmul-rN  41629  dvamulr  41827  dvavadd  41830  dvhmulr  41901  cdlemm10N  41933  repncan3  43185  pellfund14  43666  mendmulr  43952  onnoxpg  44196  fmuldfeq  46340  stoweidlem19  46774  stoweidlem26  46781  addsubeq0  48074  zp1modne  48130  modm1nep1  48149  prelspr  48276  lincval1  49240