Theorem mp3an2 1325

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

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

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 980

This theorem is referenced by:  mp3anl2  1332  ordin  4387  ordsuc  4564  omv  6459  oeiv  6460  omv2  6469  1idprl  7592  muladd11  8093  negsub  8208  subneg  8209  ltaddneg  8384  muleqadd  8628  diveqap1  8665  conjmulap  8689  nnsub  8961  addltmul  9158  zltp1le  9310  gtndiv  9351  eluzp1m1  9554  xnn0le2is012  9869  divelunit  10005  fznatpl1  10079  flqbi2  10294  flqdiv  10324  frecfzen2  10430  nn0ennn  10436  faclbnd3  10726  shftfvalg  10830  ovshftex  10831  shftfval  10833  abs2dif  11118  cos2t  11761  sin01gt0  11772  cos01gt0  11773  demoivre  11783  demoivreALT  11784  omeo  11906  gcd0id  11983  sqgcd  12033  isprm3  12121  eulerthlemth  12235  pczpre  12300  pcrec  12311  setscom  12505  setsslid  12516  setsslnid  12517  mulgm1  13013  abssinper  14428  lgs1  14606