ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5 Unicode version

Theorem syl5 32
Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)
Hypotheses
Ref Expression
syl5.1  |-  ( ph  ->  ps )
syl5.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5
StepHypRef Expression
1 syl5.1 . . 3  |-  ( ph  ->  ps )
2 syl5.2 . . 3  |-  ( ch 
->  ( ps  ->  th )
)
31, 2syl5com 29 . 2  |-  ( ph  ->  ( ch  ->  th )
)
43com12 30 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syl56  34  syl2im  38  imim12i  57  pm2.86d  97  syl5bi  145  syl5bir  146  syl5ib  147  adantld  267  adantrd  268  mpan9  269  nsyli  588  pm2.36  728  pm4.72  747  pm2.18dc  761  con1dc  764  jadc  771  pm2.521dc  775  con1biimdc  778  condandc  786  pm5.18dc  788  pm2.68dc  804  annimdc  856  syl3an2  1180  xor3dc  1294  alrimdh  1384  spsd  1447  a5i  1451  19.21h  1465  hbnt  1559  hbae  1622  sbiedh  1686  exdistrfor  1697  sbcof2  1707  ax11a2  1718  ax11v  1724  sb4  1729  hbsb4t  1905  exmoeudc  1979  euimmo  1983  mopick  1994  r19.37  2479  spcimgft  2646  spcimegft  2648  rr19.28v  2706  mob2  2744  euind  2751  reuind  2767  sbeqalb  2842  triun  3895  csbexga  3913  copsexg  4009  trssord  4145  trsuc  4187  trsucss  4188  ralxfrd  4222  rexxfrd  4223  ralxfrALT  4227  sucprcreg  4301  nlimsucg  4318  tfis  4334  relssres  4676  issref  4735  dmsnopg  4820  dfco2a  4849  imadif  5007  fvelima  5253  mptfvex  5284  fvmptdf  5286  fvmptf  5291  foco2  5346  funfvima2  5419  funfvima3  5420  isores3  5483  oprabid  5565  ovmpt4g  5651  ovmpt2s  5652  ov2gf  5653  ovmpt2df  5660  suppssfv  5736  suppssov1  5737  fo2ndf  5876  rntpos  5903  tposf2  5914  nnmordi  6120  nnmord  6121  nnaordex  6131  ectocld  6203  qsel  6214  f1oeng  6268  nneneq  6351  findcard2  6377  findcard2s  6378  ac6sfi  6383  ltbtwnnqq  6571  prnmaddl  6646  genpcdl  6675  genpcuu  6676  ltaddpr  6753  lteupri  6773  recexprlemss1l  6791  recexprlemss1u  6792  cauappcvgprlemdisj  6807  lttrsr  6905  recexgt0sr  6916  mulgt0sr  6920  axprecex  7012  rereceu  7021  addlsub  7440  recexap  7708  0mnnnnn0  8271  prime  8396  zeo  8402  fnn0ind  8413  zindd  8415  btwnz  8416  lbzbi  8648  addmodlteq  9348  facwordi  9608  qdenre  10029  climcau  10097  serif0  10102  odd2np1  10184  ndvdssub  10242  bj-sbimedh  10298  bj-vtoclgft  10301  elabgft1  10304  elabgf2  10306
  Copyright terms: Public domain W3C validator