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 1119	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 687	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  1775  elovmpo  7678  f1oeng  9011  php  9247  nnsdomg  9335  wdomimag  9627  gruuni  10840  genpv  11039  pncan3  11516  mulsubaddmulsub  11727  infssuzle  12973  fzrevral3  13654  flflp1  13847  subsq2  14250  brfi1ind  14548  opfi1ind  14551  ccatws1ls  14671  swrdrlen  14697  pfxpfxid  14747  pfxcctswrd  14748  2cshwid  14852  caubnd  15397  dvdsmul1  16315  dvdsmul2  16316  hashbcval  17040  setsvalg  17203  ressval  17277  restval  17471  mrelatglb0  18606  imasmnd2  18787  efmndov  18894  qusinv  19208  ghminv  19241  gsmsymgrfixlem1  19445  gsmsymgreqlem2  19449  gexod  19604  lsmvalx  19657  rngrz  20163  imasring  20327  irredneg  20430  01eq0ring  20530  ocvin  21692  frlmiscvec  21869  evlrhm  22120  gsumsmonply1  22311  mat1mhm  22490  marrepfval  22566  marrepval0  22567  marepvfval  22571  marepvval0  22572  1elcpmat  22721  m2cpminv0  22767  idpm2idmp  22807  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  restin  23174  qtopval  23703  elqtop3  23711  elfm3  23958  flimval  23971  nmge0  24630  nmeq0  24631  nminv  24634  nmo0  24756  0nghm  24762  coemulhi  26293  isosctrlem2  26862  divsqrtsumlem  27023  2lgsoddprmlem4  27459  0uhgrrusgr  29596  frgruhgr0v  30283  nvge0  30692  nvnd  30707  dip0r  30736  dip0l  30737  nmoo0  30810  hi2eq  31124  wrdsplex  32920  resvval  33353  unitdivcld  33900  signspval  34567  satfv0  35363  ltflcei  37615  elghomlem1OLD  37892  rngorz  37930  rngonegmn1l  37948  rngonegmn1r  37949  igenval  38068  xrnidresex  38408  xrncnvepresex  38409  lfl0  39066  olj01  39226  olm11  39228  hl2at  39407  pmapeq0  39768  trlcl  40166  trlle  40186  tendoid  40775  tendo0plr  40794  tendoipl2  40800  erngmul  40808  erngmul-rN  40816  dvamulr  41014  dvavadd  41017  dvhmulr  41088  cdlemm10N  41120  repncan3  42413  pellfund14  42909  mendmulr  43196  onnog  43442  fmuldfeq  45598  stoweidlem19  46034  stoweidlem26  46041  addsubeq0  47308  zp1modne  47348  prelspr  47473  lincval1  48336