Theorem mp3an2 1359

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 1227	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 435	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

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 1004

This theorem is referenced by:  mp3anl2  1366  ordin  4476  ordsuc  4655  omv  6609  oeiv  6610  omv2  6619  1idprl  7788  muladd11  8290  negsub  8405  subneg  8406  ltaddneg  8582  muleqadd  8826  diveqap1  8863  conjmulap  8887  nnsub  9160  addltmul  9359  zltp1le  9512  gtndiv  9553  eluzp1m1  9758  xnn0le2is012  10074  divelunit  10210  fznatpl1  10284  flqbi2  10523  flqdiv  10555  frecfzen2  10661  nn0ennn  10667  seqshft2g  10716  seqf1oglem1  10753  faclbnd3  10977  ccatrid  11155  shftfvalg  11345  ovshftex  11346  shftfval  11348  abs2dif  11633  cos2t  12277  sin01gt0  12289  cos01gt0  12290  demoivre  12300  demoivreALT  12301  omeo  12425  gcd0id  12516  sqgcd  12566  isprm3  12656  eulerthlemth  12770  pczpre  12836  pcrec  12847  setscom  13088  setsslid  13099  setsslnid  13100  mulgm1  13695  abssinper  15536  lgs1  15739