Theorem mpd3an3 1459

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  stoic2b  1770  elovmpo  7661  f1oeng  8986  php  9229  nnsdomg  9321  wdomimag  9605  gruuni  10818  genpv  11017  pncan3  11493  mulsubaddmulsub  11703  infssuzle  12940  fzrevral3  13615  flflp1  13799  subsq2  14201  brfi1ind  14487  opfi1ind  14490  ccatws1ls  14610  swrdrlen  14636  pfxpfxid  14686  pfxcctswrd  14687  2cshwid  14791  caubnd  15332  dvdsmul1  16249  dvdsmul2  16250  hashbcval  16965  setsvalg  17129  ressval  17206  restval  17402  mrelatglb0  18547  imasmnd2  18725  efmndov  18827  qusinv  19139  ghminv  19171  gsmsymgrfixlem1  19376  gsmsymgreqlem2  19380  gexod  19535  lsmvalx  19588  rngrz  20100  imasring  20260  irredneg  20363  01eq0ring  20461  ocvin  21600  frlmiscvec  21777  evlrhm  22036  gsumsmonply1  22220  mat1mhm  22380  marrepfval  22456  marrepval0  22457  marepvfval  22461  marepvval0  22462  1elcpmat  22611  m2cpminv0  22657  idpm2idmp  22697  chfacfscmulgsum  22756  chfacfpmmulgsum  22760  restin  23064  qtopval  23593  elqtop3  23601  elfm3  23848  flimval  23861  nmge0  24520  nmeq0  24521  nminv  24524  nmo0  24646  0nghm  24652  coemulhi  26182  isosctrlem2  26745  divsqrtsumlem  26906  2lgsoddprmlem4  27342  0uhgrrusgr  29386  frgruhgr0v  30068  nvge0  30477  nvnd  30492  dip0r  30521  dip0l  30522  nmoo0  30595  hi2eq  30909  wrdsplex  32656  resvval  33033  unitdivcld  33497  signspval  34179  satfv0  34963  ltflcei  37076  elghomlem1OLD  37353  rngorz  37391  rngonegmn1l  37409  rngonegmn1r  37410  igenval  37529  xrnidresex  37874  xrncnvepresex  37875  lfl0  38532  olj01  38692  olm11  38694  hl2at  38873  pmapeq0  39234  trlcl  39632  trlle  39652  tendoid  40241  tendo0plr  40260  tendoipl2  40266  erngmul  40274  erngmul-rN  40282  dvamulr  40480  dvavadd  40483  dvhmulr  40554  cdlemm10N  40586  repncan3  41929  pellfund14  42309  mendmulr  42603  onnog  42850  fmuldfeq  44962  stoweidlem19  45398  stoweidlem26  45405  addsubeq0  46667  prelspr  46817  lincval1  47478