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  4480  ordsuc  4659  omv  6618  oeiv  6619  omv2  6628  1idprl  7800  muladd11  8302  negsub  8417  subneg  8418  ltaddneg  8594  muleqadd  8838  diveqap1  8875  conjmulap  8899  nnsub  9172  addltmul  9371  zltp1le  9524  gtndiv  9565  eluzp1m1  9770  xnn0le2is012  10091  divelunit  10227  fznatpl1  10301  flqbi2  10541  flqdiv  10573  frecfzen2  10679  nn0ennn  10685  seqshft2g  10734  seqf1oglem1  10771  faclbnd3  10995  ccatrid  11174  shftfvalg  11369  ovshftex  11370  shftfval  11372  abs2dif  11657  cos2t  12301  sin01gt0  12313  cos01gt0  12314  demoivre  12324  demoivreALT  12325  omeo  12449  gcd0id  12540  sqgcd  12590  isprm3  12680  eulerthlemth  12794  pczpre  12860  pcrec  12871  setscom  13112  setsslid  13123  setsslnid  13124  mulgm1  13719  abssinper  15560  lgs1  15763