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  4506  ordsuc  4685  omv  6688  oeiv  6689  omv2  6698  1idprl  7905  muladd11  8406  negsub  8521  subneg  8522  ltaddneg  8698  muleqadd  8942  diveqap1  8979  conjmulap  9003  nnsub  9276  addltmul  9475  zltp1le  9632  gtndiv  9673  eluzp1m1  9878  xnn0le2is012  10199  divelunit  10335  fznatpl1  10410  flqbi2  10651  flqdiv  10683  frecfzen2  10789  nn0ennn  10795  seqshft2g  10844  seqf1oglem1  10881  faclbnd3  11105  ccatrid  11295  shftfvalg  11503  ovshftex  11504  shftfval  11506  abs2dif  11791  cos2t  12436  sin01gt0  12448  cos01gt0  12449  demoivre  12459  demoivreALT  12460  omeo  12584  gcd0id  12675  sqgcd  12725  isprm3  12815  eulerthlemth  12929  pczpre  12995  pcrec  13006  setscom  13252  setsslid  13263  setsslnid  13264  mulgm1  13859  abssinper  15711  lgs1  15917