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  7573  addnnnq0  7817  mulnnnq0  7818  prarloclemcalc  7870  genpelxp  7879  genpprecll  7882  genppreclu  7883  addsrpr  8113  mulsrpr  8114  gt0srpr  8116  mulrid  8324  ltneg  8792  leneg  8795  suble0  8806  div1  9036  nnaddcl  9327  nnmulcl  9328  nnge1  9330  nnsub  9346  2halves  9539  halfaddsub  9544  addltmul  9547  fcdmnn0fsuppg  9623  zleltp1  9705  nnaddm1cl  9711  zextlt  9743  peano5uzti  9759  eluzp1p1  9958  uzaddcl  9996  znq  10034  xrre  10233  xrre2  10234  fzshftral  10526  nninfinf  10894  expn1ap0  11000  expadd  11032  expmul  11035  expubnd  11047  sqmul  11052  bernneq  11112  sqrecapd  11129  faclbnd2  11195  faclbnd6  11197  fihashssdif  11274  ccatlcan  11505  ccatrcan  11506  shftval3  11607  caucvgre  11762  leabs  11855  ltabs  11869  caubnd2  11899  efexp  12467  efival  12517  cos01gt0  12548  odd2np1  12658  halfleoddlt  12679  omoe  12681  opeo  12682  gcdmultiple  12815  sqgcd  12824  nn0seqcvgd  12837  phiprmpw  13022  eulerthlemth  13032  odzcllem  13043  pcelnn  13122  4sqlem3  13191  lsp0  14811  lss0v  14818  zndvds0  15036  ntrin  15277  txuni2  15409  txopn  15418  xblpnfps  15551  xblpnf  15552  bl2in  15556  unirnblps  15575  unirnbl  15576  blpnfctr  15592  plyconst  15898  plyid  15899  sincosq1eq  15993  rpcxpp1  16064  rplogb1  16106  ppiqub  16215  bposlem1  16233  bposlem2  16234