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  7598  f1oeng  8903  php  9131  nnsdomg  9204  wdomimag  9498  gruuni  10713  genpv  10912  pncan3  11389  mulsubaddmulsub  11602  infssuzle  12850  fzrevral3  13535  flflp1  13729  subsq2  14136  brfi1ind  14434  opfi1ind  14437  ccatws1ls  14558  swrdrlen  14584  pfxpfxid  14633  pfxcctswrd  14634  2cshwid  14738  caubnd  15284  dvdsmul1  16206  dvdsmul2  16207  hashbcval  16932  setsvalg  17095  ressval  17162  restval  17348  mrelatglb0  18485  imasmnd2  18666  efmndov  18773  qusinv  19087  ghminv  19120  gsmsymgrfixlem1  19324  gsmsymgreqlem2  19328  gexod  19483  lsmvalx  19536  rngrz  20069  imasring  20233  irredneg  20333  01eq0ring  20433  ocvin  21599  frlmiscvec  21774  evlrhm  22019  gsumsmonply1  22210  mat1mhm  22387  marrepfval  22463  marrepval0  22464  marepvfval  22468  marepvval0  22469  1elcpmat  22618  m2cpminv0  22664  idpm2idmp  22704  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  restin  23069  qtopval  23598  elqtop3  23606  elfm3  23853  flimval  23866  nmge0  24521  nmeq0  24522  nminv  24525  nmo0  24639  0nghm  24645  coemulhi  26175  isosctrlem2  26745  divsqrtsumlem  26906  2lgsoddprmlem4  27342  0uhgrrusgr  29542  frgruhgr0v  30226  nvge0  30635  nvnd  30650  dip0r  30679  dip0l  30680  nmoo0  30753  hi2eq  31067  wrdsplex  32890  resvval  33277  unitdivcld  33867  signspval  34519  satfv0  35330  ltflcei  37587  elghomlem1OLD  37864  rngorz  37902  rngonegmn1l  37920  rngonegmn1r  37921  igenval  38040  xrnidresex  38378  xrncnvepresex  38379  lfl0  39043  olj01  39203  olm11  39205  hl2at  39384  pmapeq0  39745  trlcl  40143  trlle  40163  tendoid  40752  tendo0plr  40771  tendoipl2  40777  erngmul  40785  erngmul-rN  40793  dvamulr  40991  dvavadd  40994  dvhmulr  41065  cdlemm10N  41097  repncan3  42356  pellfund14  42871  mendmulr  43157  onnog  43402  fmuldfeq  45565  stoweidlem19  46001  stoweidlem26  46008  addsubeq0  47281  zp1modne  47331  modm1nep1  47350  prelspr  47471  lincval1  48405