Theorem mp3an2 1362

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

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

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 1007

This theorem is referenced by:  mp3anl2  1369  ordin  4488  ordsuc  4667  omv  6666  oeiv  6667  omv2  6676  1idprl  7870  muladd11  8371  negsub  8486  subneg  8487  ltaddneg  8663  muleqadd  8907  diveqap1  8944  conjmulap  8968  nnsub  9241  addltmul  9440  zltp1le  9595  gtndiv  9636  eluzp1m1  9841  xnn0le2is012  10162  divelunit  10298  fznatpl1  10373  flqbi2  10614  flqdiv  10646  frecfzen2  10752  nn0ennn  10758  seqshft2g  10807  seqf1oglem1  10844  faclbnd3  11068  ccatrid  11250  shftfvalg  11458  ovshftex  11459  shftfval  11461  abs2dif  11746  cos2t  12391  sin01gt0  12403  cos01gt0  12404  demoivre  12414  demoivreALT  12415  omeo  12539  gcd0id  12630  sqgcd  12680  isprm3  12770  eulerthlemth  12884  pczpre  12950  pcrec  12961  setscom  13202  setsslid  13213  setsslnid  13214  mulgm1  13809  abssinper  15657  lgs1  15863