Theorem mp3an2 1362

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 1230	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 435	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

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 1007

This theorem is referenced by:  mp3anl2  1369  ordin  4505  ordsuc  4684  omv  6687  oeiv  6688  omv2  6697  1idprl  7901  muladd11  8402  negsub  8517  subneg  8518  ltaddneg  8694  muleqadd  8938  diveqap1  8975  conjmulap  8999  nnsub  9272  addltmul  9471  zltp1le  9628  gtndiv  9669  eluzp1m1  9874  xnn0le2is012  10195  divelunit  10331  fznatpl1  10406  flqbi2  10647  flqdiv  10679  frecfzen2  10785  nn0ennn  10791  seqshft2g  10840  seqf1oglem1  10877  faclbnd3  11101  ccatrid  11288  shftfvalg  11496  ovshftex  11497  shftfval  11499  abs2dif  11784  cos2t  12429  sin01gt0  12441  cos01gt0  12442  demoivre  12452  demoivreALT  12453  omeo  12577  gcd0id  12668  sqgcd  12718  isprm3  12808  eulerthlemth  12922  pczpre  12988  pcrec  12999  setscom  13241  setsslid  13252  setsslnid  13253  mulgm1  13848  abssinper  15698  lgs1  15904