Theorem mpd3an3 1486

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  stoic2b  1798  elovmpo  7645  f1oeng  8955  php  9179  nnsdomg  9247  wdomimag  9537  gruuni  10773  genpv  10972  pncan3  11453  mulsubaddmulsub  11666  infssuzle  12946  fzrevral3  13633  flflp1  13831  subsq2  14238  brfi1ind  14536  opfi1ind  14539  ccatws1ls  14661  swrdrlen  14687  pfxpfxid  14736  pfxcctswrd  14737  2cshwid  14841  caubnd  15400  dvdsmul1  16325  dvdsmul2  16326  hashbcval  17052  setsvalg  17216  ressval  17283  restval  17469  mrelatglb0  18607  imasmnd2  18822  efmndov  18930  qusinv  19252  ghminv  19284  gsmsymgrfixlem1  19488  gsmsymgreqlem2  19492  gexod  19647  lsmvalx  19700  rngrz  20235  imasring  20403  irredneg  20503  01eq0ring  20605  ocvin  21784  frlmiscvec  21959  evlrhm  22212  gsumsmonply1  22428  mat1mhm  22602  marrepfval  22678  marrepval0  22679  marepvfval  22683  marepvval0  22684  1elcpmat  22833  m2cpminv0  22879  idpm2idmp  22919  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  restin  23284  qtopval  23813  elqtop3  23821  elfm3  24068  flimval  24081  nmge0  24735  nmeq0  24736  nminv  24739  nmo0  24853  0nghm  24859  coemulhi  26372  isosctrlem2  26942  divsqrtsumlem  27102  2lgsoddprmlem4  27537  0uhgrrusgr  29837  frgruhgr0v  30524  nvge0  30934  nvnd  30949  dip0r  30978  dip0l  30979  nmoo0  31052  hi2eq  31366  wrdsplex  33169  resvval  33564  unitdivcld  34208  signspval  34856  satfv0  35721  ltflcei  38119  elghomlem1OLD  38396  rngorz  38434  rngonegmn1l  38452  rngonegmn1r  38453  igenval  38572  xrnidresex  38941  xrncnvepresex  38942  lfl0  39701  olj01  39861  olm11  39863  hl2at  40041  pmapeq0  40402  trlcl  40800  trlle  40820  tendoid  41409  tendo0plr  41428  tendoipl2  41434  erngmul  41442  erngmul-rN  41450  dvamulr  41648  dvavadd  41651  dvhmulr  41722  cdlemm10N  41754  repncan3  43004  pellfund14  43487  mendmulr  43773  onnoxpg  44017  fmuldfeq  46157  stoweidlem19  46591  stoweidlem26  46598  addsubeq0  47888  zp1modne  47944  modm1nep1  47963  prelspr  48090  lincval1  49050