Theorem mp3an2 1320

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

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

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

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

This theorem is referenced by:  mp3anl2  1327  ordin  4368  ordsuc  4545  omv  6432  oeiv  6433  omv2  6442  1idprl  7545  muladd11  8045  negsub  8160  subneg  8161  ltaddneg  8336  muleqadd  8579  diveqap1  8615  conjmulap  8639  nnsub  8910  addltmul  9107  zltp1le  9259  gtndiv  9300  eluzp1m1  9503  xnn0le2is012  9816  divelunit  9952  fznatpl1  10025  flqbi2  10240  flqdiv  10270  frecfzen2  10376  nn0ennn  10382  faclbnd3  10670  shftfvalg  10775  ovshftex  10776  shftfval  10778  abs2dif  11063  cos2t  11706  sin01gt0  11717  cos01gt0  11718  demoivre  11728  demoivreALT  11729  omeo  11850  gcd0id  11927  sqgcd  11977  isprm3  12065  eulerthlemth  12179  pczpre  12244  pcrec  12255  setscom  12449  setsslid  12459  setsslnid  12460  abssinper  13526  lgs1  13704