Theorem mp3an2 1314

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

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

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 969

This theorem is referenced by:  mp3anl2  1321  ordin  4357  ordsuc  4534  omv  6414  oeiv  6415  omv2  6424  1idprl  7522  muladd11  8022  negsub  8137  subneg  8138  ltaddneg  8313  muleqadd  8556  diveqap1  8592  conjmulap  8616  nnsub  8887  addltmul  9084  zltp1le  9236  gtndiv  9277  eluzp1m1  9480  xnn0le2is012  9793  divelunit  9929  fznatpl1  10001  flqbi2  10216  flqdiv  10246  frecfzen2  10352  nn0ennn  10358  faclbnd3  10645  shftfvalg  10746  ovshftex  10747  shftfval  10749  abs2dif  11034  cos2t  11677  sin01gt0  11688  cos01gt0  11689  demoivre  11699  demoivreALT  11700  omeo  11820  gcd0id  11897  sqgcd  11947  isprm3  12029  eulerthlemth  12141  pczpre  12206  pcrec  12217  setscom  12371  setsslid  12381  setsslnid  12382  abssinper  13308