Theorem mp3an3 1337

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 1207	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> 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:  mp3an13  1339  mp3an23  1340  mp3anl3  1344  opelxp  4693  funimaexg  5342  ov  6042  ovmpoa  6053  ovmpo  6058  ovtposg  6317  oaword1  6529  th3q  6699  enrefg  6823  f1imaen  6853  mapxpen  6909  pw1fin  6971  xpfi  6993  djucomen  7283  addnnnq0  7516  mulnnnq0  7517  prarloclemcalc  7569  genpelxp  7578  genpprecll  7581  genppreclu  7582  addsrpr  7812  mulsrpr  7813  gt0srpr  7815  mulrid  8023  ltneg  8489  leneg  8492  suble0  8503  div1  8730  nnaddcl  9010  nnmulcl  9011  nnge1  9013  nnsub  9029  2halves  9220  halfaddsub  9225  addltmul  9228  zleltp1  9381  nnaddm1cl  9387  zextlt  9418  peano5uzti  9434  eluzp1p1  9627  uzaddcl  9660  znq  9698  xrre  9895  xrre2  9896  fzshftral  10183  nninfinf  10535  expn1ap0  10641  expadd  10673  expmul  10676  expubnd  10688  sqmul  10693  bernneq  10752  sqrecapd  10769  faclbnd2  10834  faclbnd6  10836  fihashssdif  10910  shftval3  10992  caucvgre  11146  leabs  11239  ltabs  11252  caubnd2  11282  efexp  11847  efival  11897  cos01gt0  11928  odd2np1  12038  halfleoddlt  12059  omoe  12061  opeo  12062  gcdmultiple  12187  sqgcd  12196  nn0seqcvgd  12209  phiprmpw  12390  eulerthlemth  12400  odzcllem  12411  pcelnn  12490  4sqlem3  12559  lsp0  13979  lss0v  13986  zndvds0  14206  ntrin  14360  txuni2  14492  txopn  14501  xblpnfps  14634  xblpnf  14635  bl2in  14639  unirnblps  14658  unirnbl  14659  blpnfctr  14675  plyconst  14981  plyid  14982  sincosq1eq  15075  rpcxpp1  15142  rplogb1  15184