Theorem mp3an2 1338

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	⊢ 𝜓
mp3an2.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 ⊢ 𝜓
2		mp3an2.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1206	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 435	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

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 983

This theorem is referenced by:  mp3anl2  1345  ordin  4450  ordsuc  4629  omv  6564  oeiv  6565  omv2  6574  1idprl  7738  muladd11  8240  negsub  8355  subneg  8356  ltaddneg  8532  muleqadd  8776  diveqap1  8813  conjmulap  8837  nnsub  9110  addltmul  9309  zltp1le  9462  gtndiv  9503  eluzp1m1  9707  xnn0le2is012  10023  divelunit  10159  fznatpl1  10233  flqbi2  10471  flqdiv  10503  frecfzen2  10609  nn0ennn  10615  seqshft2g  10664  seqf1oglem1  10701  faclbnd3  10925  ccatrid  11101  shftfvalg  11244  ovshftex  11245  shftfval  11247  abs2dif  11532  cos2t  12176  sin01gt0  12188  cos01gt0  12189  demoivre  12199  demoivreALT  12200  omeo  12324  gcd0id  12415  sqgcd  12465  isprm3  12555  eulerthlemth  12669  pczpre  12735  pcrec  12746  setscom  12987  setsslid  12998  setsslnid  12999  mulgm1  13593  abssinper  15433  lgs1  15636