Theorem mp3an3 1367

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 1236	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> th )

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

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 1011

This theorem is referenced by:  mp3an13  1369  mp3an23  1370  mp3anl3  1374  opelxp  4802  funimaexg  5463  ov  6201  ovmpoa  6212  ovmpo  6217  ovtposg  6523  oaword1  6737  th3q  6907  enrefg  7043  f1imaen  7074  mapxpen  7141  pw1fin  7210  xpfi  7232  djucomen  7565  addnnnq0  7809  mulnnnq0  7810  prarloclemcalc  7862  genpelxp  7871  genpprecll  7874  genppreclu  7875  addsrpr  8105  mulsrpr  8106  gt0srpr  8108  mulrid  8316  ltneg  8783  leneg  8786  suble0  8797  div1  9026  nnaddcl  9306  nnmulcl  9307  nnge1  9309  nnsub  9325  2halves  9516  halfaddsub  9521  addltmul  9524  fcdmnn0fsuppg  9600  zleltp1  9682  nnaddm1cl  9688  zextlt  9720  peano5uzti  9736  eluzp1p1  9930  uzaddcl  9968  znq  10006  xrre  10204  xrre2  10205  fzshftral  10496  nninfinf  10861  expn1ap0  10967  expadd  10999  expmul  11002  expubnd  11014  sqmul  11019  bernneq  11079  sqrecapd  11096  faclbnd2  11161  faclbnd6  11163  fihashssdif  11240  ccatlcan  11471  ccatrcan  11472  shftval3  11573  caucvgre  11728  leabs  11821  ltabs  11834  caubnd2  11864  efexp  12430  efival  12480  cos01gt0  12511  odd2np1  12621  halfleoddlt  12642  omoe  12644  opeo  12645  gcdmultiple  12778  sqgcd  12787  nn0seqcvgd  12800  phiprmpw  12981  eulerthlemth  12991  odzcllem  13002  pcelnn  13081  4sqlem3  13150  lsp0  14735  lss0v  14742  zndvds0  14960  ntrin  15151  txuni2  15283  txopn  15292  xblpnfps  15425  xblpnf  15426  bl2in  15430  unirnblps  15449  unirnbl  15450  blpnfctr  15466  plyconst  15772  plyid  15773  sincosq1eq  15866  rpcxpp1  15934  rplogb1  15976