Theorem mp3an3 1305

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 1184	. 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  1307  mp3an23  1308  mp3anl3  1312  opelxp  4577  funimaexg  5215  ov  5898  ovmpoa  5909  ovmpo  5914  ovtposg  6164  oaword1  6375  th3q  6542  enrefg  6666  f1imaen  6696  mapxpen  6750  xpfi  6826  djucomen  7089  addnnnq0  7281  mulnnnq0  7282  prarloclemcalc  7334  genpelxp  7343  genpprecll  7346  genppreclu  7347  addsrpr  7577  mulsrpr  7578  gt0srpr  7580  mulid1  7787  ltneg  8248  leneg  8251  suble0  8262  div1  8487  nnaddcl  8764  nnmulcl  8765  nnge1  8767  nnsub  8783  2halves  8973  halfaddsub  8978  addltmul  8980  zleltp1  9133  nnaddm1cl  9139  zextlt  9167  peano5uzti  9183  eluzp1p1  9375  uzaddcl  9408  znq  9443  xrre  9633  xrre2  9634  fzshftral  9919  expn1ap0  10334  expadd  10366  expmul  10369  expubnd  10381  sqmul  10386  bernneq  10443  sqrecapd  10459  faclbnd2  10520  faclbnd6  10522  fihashssdif  10596  shftval3  10631  caucvgre  10785  leabs  10878  ltabs  10891  caubnd2  10921  efexp  11425  efival  11475  cos01gt0  11505  odd2np1  11606  halfleoddlt  11627  omoe  11629  opeo  11630  gcdmultiple  11744  sqgcd  11753  nn0seqcvgd  11758  phiprmpw  11934  ntrin  12332  txuni2  12464  txopn  12473  xblpnfps  12606  xblpnf  12607  bl2in  12611  unirnblps  12630  unirnbl  12631  blpnfctr  12647  sincosq1eq  12968  rpcxpp1  13035  rplogb1  13073