Theorem mpd3an3 1338

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

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

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 980

This theorem is referenced by:  stoic2b  1430  elovmpo  6072  oav  6455  omv  6456  oeiv  6457  f1oeng  6757  mulpipq2  7370  ltrnqg  7419  genipv  7508  subval  8149  subap0  8600  xaddval  9845  fzrevral3  10107  fzoval  10148  subsq2  10628  bcval  10729  dvdsmul1  11820  dvdsmul2  11821  gcdval  11960  eucalgval2  12053  setsvalg  12492  restval  12694  xpsfval  12767  ismhm  12853  subsubg  13057  srglmhm  13176  ringrz  13223  01eq0ring  13330  restin  13679  hmeofvalg  13806  cncfval  14062  rpcxpef  14318  rpcxpneg  14331  lgsval  14408  2lgsoddprmlem4  14463