Theorem mp3an2 1336

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

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

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 982

This theorem is referenced by:  mp3anl2  1343  ordin  4421  ordsuc  4600  omv  6522  oeiv  6523  omv2  6532  1idprl  7676  muladd11  8178  negsub  8293  subneg  8294  ltaddneg  8470  muleqadd  8714  diveqap1  8751  conjmulap  8775  nnsub  9048  addltmul  9247  zltp1le  9399  gtndiv  9440  eluzp1m1  9644  xnn0le2is012  9960  divelunit  10096  fznatpl1  10170  flqbi2  10400  flqdiv  10432  frecfzen2  10538  nn0ennn  10544  seqshft2g  10593  seqf1oglem1  10630  faclbnd3  10854  shftfvalg  11002  ovshftex  11003  shftfval  11005  abs2dif  11290  cos2t  11934  sin01gt0  11946  cos01gt0  11947  demoivre  11957  demoivreALT  11958  omeo  12082  gcd0id  12173  sqgcd  12223  isprm3  12313  eulerthlemth  12427  pczpre  12493  pcrec  12504  setscom  12745  setsslid  12756  setsslnid  12757  mulgm1  13350  abssinper  15190  lgs1  15393