Theorem mpd3an3 1374

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  stoic2b  1474  elovmpo  6221  oav  6622  omv  6623  oeiv  6624  f1oeng  6930  mulpipq2  7591  ltrnqg  7640  genipv  7729  subval  8371  subap0  8823  xaddval  10080  fzrevral3  10342  fzoval  10383  subsq2  10910  bcval  11012  ccatws1ls  11220  swrdrlen  11243  pfxpfxid  11291  pfxcctswrd  11292  dvdsmul1  12376  dvdsmul2  12377  gcdval  12532  eucalgval2  12627  setsvalg  13114  restval  13330  xpsfval  13433  imasmnd2  13537  ismhm  13546  mhmex  13547  subsubm  13568  subsubg  13786  qusinv  13825  isghm  13832  ghminv  13839  rngrz  13962  srglmhm  14009  ringrz  14060  imasring  14080  isrhm  14175  01eq0ring  14206  restin  14903  hmeofvalg  15030  cncfval  15299  rpcxpef  15621  rpcxpneg  15634  sgmval  15710  fsumdvdsmul  15718  lgsval  15736  2lgsoddprmlem4  15844  clwwlknon  16283