Theorem mp3an3 1263

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

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

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

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

This theorem is referenced by:  mp3an13  1265  mp3an23  1266  mp3anl3  1270  opelxp  4481  funimaexg  5111  ov  5778  ovmpt2a  5789  ovmpt2  5794  ovtposg  6038  oaword1  6246  th3q  6411  enrefg  6535  f1imaen  6565  mapxpen  6618  xpfi  6694  addnnnq0  7069  mulnnnq0  7070  prarloclemcalc  7122  genpelxp  7131  genpprecll  7134  genppreclu  7135  addsrpr  7352  mulsrpr  7353  gt0srpr  7355  mulid1  7546  ltneg  8001  leneg  8004  suble0  8015  div1  8231  nnaddcl  8503  nnmulcl  8504  nnge1  8506  nnsub  8522  2halves  8706  halfaddsub  8711  addltmul  8713  zleltp1  8866  nnaddm1cl  8872  zextlt  8899  peano5uzti  8915  eluzp1p1  9105  uzaddcl  9135  znq  9170  xrre  9343  xrre2  9344  fzshftral  9583  expn1ap0  10026  expadd  10058  expmul  10061  expubnd  10073  sqmul  10078  bernneq  10135  sqrecapd  10151  faclbnd2  10211  faclbnd6  10213  fihashssdif  10287  shftval3  10322  caucvgre  10475  leabs  10568  ltabs  10581  caubnd2  10611  efexp  11033  efival  11084  cos01gt0  11114  odd2np1  11212  halfleoddlt  11233  omoe  11235  opeo  11236  gcdmultiple  11348  sqgcd  11357  nn0seqcvgd  11362  phiprmpw  11537  ntrin  11885