Theorem mp3an2 1361

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 1229	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 435	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:  mp3anl2  1368  ordin  4482  ordsuc  4661  omv  6622  oeiv  6623  omv2  6632  1idprl  7809  muladd11  8311  negsub  8426  subneg  8427  ltaddneg  8603  muleqadd  8847  diveqap1  8884  conjmulap  8908  nnsub  9181  addltmul  9380  zltp1le  9533  gtndiv  9574  eluzp1m1  9779  xnn0le2is012  10100  divelunit  10236  fznatpl1  10310  flqbi2  10550  flqdiv  10582  frecfzen2  10688  nn0ennn  10694  seqshft2g  10743  seqf1oglem1  10780  faclbnd3  11004  ccatrid  11183  shftfvalg  11378  ovshftex  11379  shftfval  11381  abs2dif  11666  cos2t  12310  sin01gt0  12322  cos01gt0  12323  demoivre  12333  demoivreALT  12334  omeo  12458  gcd0id  12549  sqgcd  12599  isprm3  12689  eulerthlemth  12803  pczpre  12869  pcrec  12880  setscom  13121  setsslid  13132  setsslnid  13133  mulgm1  13728  abssinper  15569  lgs1  15772