Theorem mp3an2 1366

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3anl2  1373  ordin  4532  ordsuc  4712  omv  6732  oeiv  6733  omv2  6742  1idprl  7964  muladd11  8467  negsub  8582  subneg  8583  ltaddneg  8760  muleqadd  9007  diveqap1  9044  conjmulap  9068  nnsub  9353  addltmul  9554  zltp1le  9711  gtndiv  9753  eluzp1m1  9963  xnn0le2is012  10286  divelunit  10422  fznatpl1  10501  flqbi2  10748  flqdiv  10780  frecfzen2  10886  nn0ennn  10892  seqshft2g  10941  seqf1oglem1  10978  faclbnd3  11204  ccatrid  11398  shftfvalg  11606  ovshftex  11607  shftfval  11609  abs2dif  11896  cos2t  12543  sin01gt0  12555  cos01gt0  12556  demoivre  12566  demoivreALT  12567  omeo  12691  gcd0id  12782  sqgcd  12832  isprm3  12922  eulerthlemth  13040  pczpre  13106  pcrec  13117  setscom  13451  setsslid  13462  setsslnid  13463  mulgm1  14005  abssinper  16085  ppiqub  16305  chtqub  16308  bposlem2  16324  lgs1  16380