Theorem mp3an2 1336

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	|- ps
mp3an2.2	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an2	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 |- ps
2		mp3an2.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expa 1205	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 435	1 |- ( ( ph /\ ch ) -> th )

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  4417  ordsuc  4596  omv  6510  oeiv  6511  omv2  6520  1idprl  7652  muladd11  8154  negsub  8269  subneg  8270  ltaddneg  8445  muleqadd  8689  diveqap1  8726  conjmulap  8750  nnsub  9023  addltmul  9222  zltp1le  9374  gtndiv  9415  eluzp1m1  9619  xnn0le2is012  9935  divelunit  10071  fznatpl1  10145  flqbi2  10363  flqdiv  10395  frecfzen2  10501  nn0ennn  10507  seqshft2g  10556  seqf1oglem1  10593  faclbnd3  10817  shftfvalg  10965  ovshftex  10966  shftfval  10968  abs2dif  11253  cos2t  11896  sin01gt0  11908  cos01gt0  11909  demoivre  11919  demoivreALT  11920  omeo  12042  gcd0id  12119  sqgcd  12169  isprm3  12259  eulerthlemth  12373  pczpre  12438  pcrec  12449  setscom  12661  setsslid  12672  setsslnid  12673  mulgm1  13215  abssinper  15022  lgs1  15201