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  7634  f1oeng  8942  php  9171  nnsdomg  9246  wdomimag  9540  gruuni  10753  genpv  10952  pncan3  11429  mulsubaddmulsub  11642  infssuzle  12890  fzrevral3  13575  flflp1  13769  subsq2  14176  brfi1ind  14474  opfi1ind  14477  ccatws1ls  14598  swrdrlen  14624  pfxpfxid  14674  pfxcctswrd  14675  2cshwid  14779  caubnd  15325  dvdsmul1  16247  dvdsmul2  16248  hashbcval  16973  setsvalg  17136  ressval  17203  restval  17389  mrelatglb0  18520  imasmnd2  18701  efmndov  18808  qusinv  19122  ghminv  19155  gsmsymgrfixlem1  19357  gsmsymgreqlem2  19361  gexod  19516  lsmvalx  19569  rngrz  20075  imasring  20239  irredneg  20339  01eq0ring  20439  ocvin  21583  frlmiscvec  21758  evlrhm  22003  gsumsmonply1  22194  mat1mhm  22371  marrepfval  22447  marrepval0  22448  marepvfval  22452  marepvval0  22453  1elcpmat  22602  m2cpminv0  22648  idpm2idmp  22688  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  restin  23053  qtopval  23582  elqtop3  23590  elfm3  23837  flimval  23850  nmge0  24505  nmeq0  24506  nminv  24509  nmo0  24623  0nghm  24629  coemulhi  26159  isosctrlem2  26729  divsqrtsumlem  26890  2lgsoddprmlem4  27326  0uhgrrusgr  29506  frgruhgr0v  30193  nvge0  30602  nvnd  30617  dip0r  30646  dip0l  30647  nmoo0  30720  hi2eq  31034  wrdsplex  32857  resvval  33301  unitdivcld  33891  signspval  34543  satfv0  35345  ltflcei  37602  elghomlem1OLD  37879  rngorz  37917  rngonegmn1l  37935  rngonegmn1r  37936  igenval  38055  xrnidresex  38393  xrncnvepresex  38394  lfl0  39058  olj01  39218  olm11  39220  hl2at  39399  pmapeq0  39760  trlcl  40158  trlle  40178  tendoid  40767  tendo0plr  40786  tendoipl2  40792  erngmul  40800  erngmul-rN  40808  dvamulr  41006  dvavadd  41009  dvhmulr  41080  cdlemm10N  41112  repncan3  42371  pellfund14  42886  mendmulr  43173  onnog  43418  fmuldfeq  45581  stoweidlem19  46017  stoweidlem26  46024  addsubeq0  47297  zp1modne  47347  modm1nep1  47366  prelspr  47487  lincval1  48408