Theorem mpd3an3 1482

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  stoic2b  1794  elovmpo  7637  f1oeng  8947  php  9171  nnsdomg  9239  wdomimag  9532  gruuni  10755  genpv  10954  pncan3  11435  mulsubaddmulsub  11648  infssuzle  12929  fzrevral3  13616  flflp1  13814  subsq2  14221  brfi1ind  14519  opfi1ind  14522  ccatws1ls  14644  swrdrlen  14670  pfxpfxid  14719  pfxcctswrd  14720  2cshwid  14824  caubnd  15369  dvdsmul1  16294  dvdsmul2  16295  hashbcval  17021  setsvalg  17185  ressval  17252  restval  17438  mrelatglb0  18576  imasmnd2  18791  efmndov  18898  qusinv  19214  ghminv  19246  gsmsymgrfixlem1  19450  gsmsymgreqlem2  19454  gexod  19609  lsmvalx  19662  rngrz  20195  imasring  20358  irredneg  20458  01eq0ring  20559  ocvin  21706  frlmiscvec  21881  evlrhm  22134  gsumsmonply1  22350  mat1mhm  22524  marrepfval  22600  marrepval0  22601  marepvfval  22605  marepvval0  22606  1elcpmat  22755  m2cpminv0  22801  idpm2idmp  22841  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  restin  23206  qtopval  23735  elqtop3  23743  elfm3  23990  flimval  24003  nmge0  24657  nmeq0  24658  nminv  24661  nmo0  24775  0nghm  24781  coemulhi  26294  isosctrlem2  26861  divsqrtsumlem  27021  2lgsoddprmlem4  27456  0uhgrrusgr  29725  frgruhgr0v  30412  nvge0  30822  nvnd  30837  dip0r  30866  dip0l  30867  nmoo0  30940  hi2eq  31254  wrdsplex  33075  resvval  33476  unitdivcld  34159  signspval  34810  satfv0  35672  ltflcei  38071  elghomlem1OLD  38348  rngorz  38386  rngonegmn1l  38404  rngonegmn1r  38405  igenval  38524  xrnidresex  38893  xrncnvepresex  38894  lfl0  39653  olj01  39813  olm11  39815  hl2at  39993  pmapeq0  40354  trlcl  40752  trlle  40772  tendoid  41361  tendo0plr  41380  tendoipl2  41386  erngmul  41394  erngmul-rN  41402  dvamulr  41600  dvavadd  41603  dvhmulr  41674  cdlemm10N  41706  repncan3  42956  pellfund14  43439  mendmulr  43725  onnoxpg  43969  fmuldfeq  46123  stoweidlem19  46557  stoweidlem26  46564  addsubeq0  47854  zp1modne  47910  modm1nep1  47929  prelspr  48056  lincval1  49005