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  6623  oeiv  6624  omv2  6633  1idprl  7810  muladd11  8312  negsub  8427  subneg  8428  ltaddneg  8604  muleqadd  8848  diveqap1  8885  conjmulap  8909  nnsub  9182  addltmul  9381  zltp1le  9534  gtndiv  9575  eluzp1m1  9780  xnn0le2is012  10101  divelunit  10237  fznatpl1  10311  flqbi2  10552  flqdiv  10584  frecfzen2  10690  nn0ennn  10696  seqshft2g  10745  seqf1oglem1  10782  faclbnd3  11006  ccatrid  11188  shftfvalg  11396  ovshftex  11397  shftfval  11399  abs2dif  11684  cos2t  12329  sin01gt0  12341  cos01gt0  12342  demoivre  12352  demoivreALT  12353  omeo  12477  gcd0id  12568  sqgcd  12618  isprm3  12708  eulerthlemth  12822  pczpre  12888  pcrec  12899  setscom  13140  setsslid  13151  setsslnid  13152  mulgm1  13747  abssinper  15589  lgs1  15792