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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an13  1369  mp3an23  1370  mp3anl3  1374  opelxp  4804  funimaexg  5465  ov  6208  ovmpoa  6219  ovmpo  6224  ovtposg  6530  oaword1  6744  th3q  6914  enrefg  7050  f1imaen  7081  mapxpen  7148  pw1fin  7217  xpfi  7239  djucomen  7572  addnnnq0  7816  mulnnnq0  7817  prarloclemcalc  7869  genpelxp  7878  genpprecll  7881  genppreclu  7882  addsrpr  8112  mulsrpr  8113  gt0srpr  8115  mulrid  8323  ltneg  8791  leneg  8794  suble0  8805  div1  9035  nnaddcl  9326  nnmulcl  9327  nnge1  9329  nnsub  9345  2halves  9538  halfaddsub  9543  addltmul  9546  fcdmnn0fsuppg  9622  zleltp1  9704  nnaddm1cl  9710  zextlt  9742  peano5uzti  9758  eluzp1p1  9957  uzaddcl  9995  znq  10033  xrre  10232  xrre2  10233  fzshftral  10525  nninfinf  10893  expn1ap0  10999  expadd  11031  expmul  11034  expubnd  11046  sqmul  11051  bernneq  11111  sqrecapd  11128  faclbnd2  11194  faclbnd6  11196  fihashssdif  11273  ccatlcan  11504  ccatrcan  11505  shftval3  11606  caucvgre  11761  leabs  11854  ltabs  11868  caubnd2  11898  efexp  12465  efival  12515  cos01gt0  12546  odd2np1  12656  halfleoddlt  12677  omoe  12679  opeo  12680  gcdmultiple  12813  sqgcd  12822  nn0seqcvgd  12835  phiprmpw  13020  eulerthlemth  13030  odzcllem  13041  pcelnn  13120  4sqlem3  13189  lsp0  14809  lss0v  14816  zndvds0  15034  ntrin  15274  txuni2  15406  txopn  15415  xblpnfps  15548  xblpnf  15549  bl2in  15553  unirnblps  15572  unirnbl  15573  blpnfctr  15589  plyconst  15895  plyid  15896  sincosq1eq  15990  rpcxpp1  16061  rplogb1  16103  ppiqub  16194  bposlem1  16209  bposlem2  16210