Theorem mp3an2 1359

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

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

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 1004

This theorem is referenced by:  mp3anl2  1366  ordin  4476  ordsuc  4655  omv  6601  oeiv  6602  omv2  6611  1idprl  7777  muladd11  8279  negsub  8394  subneg  8395  ltaddneg  8571  muleqadd  8815  diveqap1  8852  conjmulap  8876  nnsub  9149  addltmul  9348  zltp1le  9501  gtndiv  9542  eluzp1m1  9746  xnn0le2is012  10062  divelunit  10198  fznatpl1  10272  flqbi2  10511  flqdiv  10543  frecfzen2  10649  nn0ennn  10655  seqshft2g  10704  seqf1oglem1  10741  faclbnd3  10965  ccatrid  11142  shftfvalg  11329  ovshftex  11330  shftfval  11332  abs2dif  11617  cos2t  12261  sin01gt0  12273  cos01gt0  12274  demoivre  12284  demoivreALT  12285  omeo  12409  gcd0id  12500  sqgcd  12550  isprm3  12640  eulerthlemth  12754  pczpre  12820  pcrec  12831  setscom  13072  setsslid  13083  setsslnid  13084  mulgm1  13679  abssinper  15520  lgs1  15723