Theorem mp3an2 1271

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 930

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 932

This theorem is referenced by:  mp3anl2  1278  ordin  4245  ordsuc  4416  omv  6281  oeiv  6282  omv2  6291  1idprl  7299  muladd11  7766  negsub  7881  subneg  7882  ltaddneg  8053  muleqadd  8290  diveqap1  8326  conjmulap  8350  nnsub  8617  addltmul  8808  zltp1le  8960  gtndiv  8998  eluzp1m1  9199  xnn0le2is012  9490  divelunit  9626  fznatpl1  9697  flqbi2  9905  flqdiv  9935  frecfzen2  10041  nn0ennn  10047  faclbnd3  10330  shftfvalg  10431  ovshftex  10432  shftfval  10434  abs2dif  10718  cos2t  11255  sin01gt0  11266  cos01gt0  11267  demoivre  11276  demoivreALT  11277  omeo  11390  gcd0id  11462  sqgcd  11510  isprm3  11592  setscom  11781  setsslid  11791  setsslnid  11792