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  10551  flqdiv  10583  frecfzen2  10689  nn0ennn  10695  seqshft2g  10744  seqf1oglem1  10781  faclbnd3  11005  ccatrid  11184  shftfvalg  11379  ovshftex  11380  shftfval  11382  abs2dif  11667  cos2t  12312  sin01gt0  12324  cos01gt0  12325  demoivre  12335  demoivreALT  12336  omeo  12460  gcd0id  12551  sqgcd  12601  isprm3  12691  eulerthlemth  12805  pczpre  12871  pcrec  12882  setscom  13123  setsslid  13134  setsslnid  13135  mulgm1  13730  abssinper  15572  lgs1  15775