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  7650  f1oeng  8983  php  9219  nnsdomg  9305  wdomimag  9599  gruuni  10812  genpv  11011  pncan3  11488  mulsubaddmulsub  11699  infssuzle  12945  fzrevral3  13629  flflp1  13822  subsq2  14227  brfi1ind  14525  opfi1ind  14528  ccatws1ls  14649  swrdrlen  14675  pfxpfxid  14725  pfxcctswrd  14726  2cshwid  14830  caubnd  15375  dvdsmul1  16295  dvdsmul2  16296  hashbcval  17020  setsvalg  17183  ressval  17252  restval  17438  mrelatglb0  18569  imasmnd2  18750  efmndov  18857  qusinv  19171  ghminv  19204  gsmsymgrfixlem1  19406  gsmsymgreqlem2  19410  gexod  19565  lsmvalx  19618  rngrz  20124  imasring  20288  irredneg  20388  01eq0ring  20488  ocvin  21632  frlmiscvec  21807  evlrhm  22052  gsumsmonply1  22243  mat1mhm  22420  marrepfval  22496  marrepval0  22497  marepvfval  22501  marepvval0  22502  1elcpmat  22651  m2cpminv0  22697  idpm2idmp  22737  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  restin  23102  qtopval  23631  elqtop3  23639  elfm3  23886  flimval  23899  nmge0  24554  nmeq0  24555  nminv  24558  nmo0  24672  0nghm  24678  coemulhi  26209  isosctrlem2  26779  divsqrtsumlem  26940  2lgsoddprmlem4  27376  0uhgrrusgr  29504  frgruhgr0v  30191  nvge0  30600  nvnd  30615  dip0r  30644  dip0l  30645  nmoo0  30718  hi2eq  31032  wrdsplex  32857  resvval  33291  unitdivcld  33878  signspval  34530  satfv0  35326  ltflcei  37578  elghomlem1OLD  37855  rngorz  37893  rngonegmn1l  37911  rngonegmn1r  37912  igenval  38031  xrnidresex  38371  xrncnvepresex  38372  lfl0  39029  olj01  39189  olm11  39191  hl2at  39370  pmapeq0  39731  trlcl  40129  trlle  40149  tendoid  40738  tendo0plr  40757  tendoipl2  40763  erngmul  40771  erngmul-rN  40779  dvamulr  40977  dvavadd  40980  dvhmulr  41051  cdlemm10N  41083  repncan3  42373  pellfund14  42868  mendmulr  43155  onnog  43400  fmuldfeq  45560  stoweidlem19  45996  stoweidlem26  46003  addsubeq0  47273  zp1modne  47323  prelspr  47448  lincval1  48343