Theorem mpd3an3 1464

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  stoic2b  1775  elovmpo  7637  f1oeng  8945  php  9177  nnsdomg  9253  wdomimag  9547  gruuni  10760  genpv  10959  pncan3  11436  mulsubaddmulsub  11649  infssuzle  12897  fzrevral3  13582  flflp1  13776  subsq2  14183  brfi1ind  14481  opfi1ind  14484  ccatws1ls  14605  swrdrlen  14631  pfxpfxid  14681  pfxcctswrd  14682  2cshwid  14786  caubnd  15332  dvdsmul1  16254  dvdsmul2  16255  hashbcval  16980  setsvalg  17143  ressval  17210  restval  17396  mrelatglb0  18527  imasmnd2  18708  efmndov  18815  qusinv  19129  ghminv  19162  gsmsymgrfixlem1  19364  gsmsymgreqlem2  19368  gexod  19523  lsmvalx  19576  rngrz  20082  imasring  20246  irredneg  20346  01eq0ring  20446  ocvin  21590  frlmiscvec  21765  evlrhm  22010  gsumsmonply1  22201  mat1mhm  22378  marrepfval  22454  marrepval0  22455  marepvfval  22459  marepvval0  22460  1elcpmat  22609  m2cpminv0  22655  idpm2idmp  22695  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  restin  23060  qtopval  23589  elqtop3  23597  elfm3  23844  flimval  23857  nmge0  24512  nmeq0  24513  nminv  24516  nmo0  24630  0nghm  24636  coemulhi  26166  isosctrlem2  26736  divsqrtsumlem  26897  2lgsoddprmlem4  27333  0uhgrrusgr  29513  frgruhgr0v  30200  nvge0  30609  nvnd  30624  dip0r  30653  dip0l  30654  nmoo0  30727  hi2eq  31041  wrdsplex  32864  resvval  33308  unitdivcld  33898  signspval  34550  satfv0  35352  ltflcei  37609  elghomlem1OLD  37886  rngorz  37924  rngonegmn1l  37942  rngonegmn1r  37943  igenval  38062  xrnidresex  38400  xrncnvepresex  38401  lfl0  39065  olj01  39225  olm11  39227  hl2at  39406  pmapeq0  39767  trlcl  40165  trlle  40185  tendoid  40774  tendo0plr  40793  tendoipl2  40799  erngmul  40807  erngmul-rN  40815  dvamulr  41013  dvavadd  41016  dvhmulr  41087  cdlemm10N  41119  repncan3  42378  pellfund14  42893  mendmulr  43180  onnog  43425  fmuldfeq  45588  stoweidlem19  46024  stoweidlem26  46031  addsubeq0  47301  zp1modne  47351  modm1nep1  47370  prelspr  47491  lincval1  48412