Theorem mp3an3 1308

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

Hypotheses

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

Assertion

Ref	Expression
mp3an3	|- ( ( ph /\ ps ) -> th )

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 |- ch
2		mp3an3.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expia 1187	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  mp3an13  1310  mp3an23  1311  mp3anl3  1315  opelxp  4613  funimaexg  5251  ov  5934  ovmpoa  5945  ovmpo  5950  ovtposg  6200  oaword1  6411  th3q  6578  enrefg  6702  f1imaen  6732  mapxpen  6786  pw1fin  6848  xpfi  6867  djucomen  7134  addnnnq0  7352  mulnnnq0  7353  prarloclemcalc  7405  genpelxp  7414  genpprecll  7417  genppreclu  7418  addsrpr  7648  mulsrpr  7649  gt0srpr  7651  mulid1  7858  ltneg  8320  leneg  8323  suble0  8334  div1  8559  nnaddcl  8836  nnmulcl  8837  nnge1  8839  nnsub  8855  2halves  9045  halfaddsub  9050  addltmul  9052  zleltp1  9205  nnaddm1cl  9211  zextlt  9239  peano5uzti  9255  eluzp1p1  9447  uzaddcl  9480  znq  9515  xrre  9706  xrre2  9707  fzshftral  9992  expn1ap0  10411  expadd  10443  expmul  10446  expubnd  10458  sqmul  10463  bernneq  10520  sqrecapd  10537  faclbnd2  10598  faclbnd6  10600  fihashssdif  10674  shftval3  10709  caucvgre  10863  leabs  10956  ltabs  10969  caubnd2  10999  efexp  11561  efival  11611  cos01gt0  11641  odd2np1  11745  halfleoddlt  11766  omoe  11768  opeo  11769  gcdmultiple  11884  sqgcd  11893  nn0seqcvgd  11898  phiprmpw  12074  eulerthlemth  12084  ntrin  12484  txuni2  12616  txopn  12625  xblpnfps  12758  xblpnf  12759  bl2in  12763  unirnblps  12782  unirnbl  12783  blpnfctr  12799  sincosq1eq  13120  rpcxpp1  13187  rplogb1  13225