Theorem mpd3an3 1462

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

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

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 1089

This theorem is referenced by:  stoic2b  1773  elovmpo  7695  f1oeng  9031  php  9273  nnsdomg  9363  wdomimag  9656  gruuni  10869  genpv  11068  pncan3  11544  mulsubaddmulsub  11754  infssuzle  12996  fzrevral3  13671  flflp1  13858  subsq2  14260  brfi1ind  14558  opfi1ind  14561  ccatws1ls  14681  swrdrlen  14707  pfxpfxid  14757  pfxcctswrd  14758  2cshwid  14862  caubnd  15407  dvdsmul1  16326  dvdsmul2  16327  hashbcval  17049  setsvalg  17213  ressval  17290  restval  17486  mrelatglb0  18631  imasmnd2  18809  efmndov  18916  qusinv  19230  ghminv  19263  gsmsymgrfixlem1  19469  gsmsymgreqlem2  19473  gexod  19628  lsmvalx  19681  rngrz  20193  imasring  20353  irredneg  20456  01eq0ring  20556  ocvin  21715  frlmiscvec  21892  evlrhm  22143  gsumsmonply1  22332  mat1mhm  22511  marrepfval  22587  marrepval0  22588  marepvfval  22592  marepvval0  22593  1elcpmat  22742  m2cpminv0  22788  idpm2idmp  22828  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  restin  23195  qtopval  23724  elqtop3  23732  elfm3  23979  flimval  23992  nmge0  24651  nmeq0  24652  nminv  24655  nmo0  24777  0nghm  24783  coemulhi  26313  isosctrlem2  26880  divsqrtsumlem  27041  2lgsoddprmlem4  27477  0uhgrrusgr  29614  frgruhgr0v  30296  nvge0  30705  nvnd  30720  dip0r  30749  dip0l  30750  nmoo0  30823  hi2eq  31137  wrdsplex  32902  resvval  33318  unitdivcld  33847  signspval  34529  satfv0  35326  ltflcei  37568  elghomlem1OLD  37845  rngorz  37883  rngonegmn1l  37901  rngonegmn1r  37902  igenval  38021  xrnidresex  38363  xrncnvepresex  38364  lfl0  39021  olj01  39181  olm11  39183  hl2at  39362  pmapeq0  39723  trlcl  40121  trlle  40141  tendoid  40730  tendo0plr  40749  tendoipl2  40755  erngmul  40763  erngmul-rN  40771  dvamulr  40969  dvavadd  40972  dvhmulr  41043  cdlemm10N  41075  repncan3  42359  pellfund14  42854  mendmulr  43145  onnog  43391  fmuldfeq  45504  stoweidlem19  45940  stoweidlem26  45947  addsubeq0  47211  prelspr  47360  lincval1  48148