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

Theorem syl5 28
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 (𝜑𝜓)
syl5.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5 (𝜒 → (𝜑𝜃))

Proof of Theorem syl5
StepHypRef Expression
1 syl5.1 . . 3 (𝜑𝜓)
2 syl5.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5com 26 . 2 (𝜑 → (𝜒𝜃))
43com12 27 1 (𝜒 → (𝜑𝜃))
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  30  syl2im  34  imim12i  53  pm2.86d  93  syl5bi  141  syl5bir  142  syl5ib  143  adantld  263  adantrd  264  mpan9  265  nsyli  578  pm2.36  717  pm4.72  736  pm2.18dc  750  con1dc  753  jadc  760  pm2.521dc  764  con1biimdc  767  condandc  775  pm5.18dc  777  pm2.68dc  793  annimdc  845  syl3an2  1169  xor3dc  1278  alrimdh  1368  spsd  1431  a5i  1435  19.21h  1449  hbnt  1543  hbae  1606  sbiedh  1670  exdistrfor  1681  sbcof2  1691  ax11a2  1702  ax11v  1708  sb4  1713  hbsb4t  1889  exmoeudc  1963  euimmo  1967  mopick  1978  r19.37  2462  spcimgft  2629  spcimegft  2631  rr19.28v  2683  mob2  2721  euind  2728  reuind  2744  sbeqalb  2815  sbcimdv  2823  triun  3867  csbexga  3885  copsexg  3981  trssord  4117  trsuc  4159  trsucss  4160  ralxfrd  4194  rexxfrd  4195  ralxfrALT  4199  sucprcreg  4273  nlimsucg  4290  tfis  4306  relssres  4648  issref  4707  dmsnopg  4792  dfco2a  4821  imadif  4979  fvelima  5225  mptfvex  5256  fvmptdf  5258  fvmptf  5263  foco2  5318  funfvima2  5391  funfvima3  5392  isores3  5455  oprabid  5537  ovmpt4g  5623  ovmpt2s  5624  ov2gf  5625  ovmpt2df  5632  suppssfv  5708  suppssov1  5709  fo2ndf  5848  rntpos  5872  tposf2  5883  nnmordi  6089  nnmord  6090  nnaordex  6100  ectocld  6172  qsel  6183  f1oeng  6237  nneneq  6320  findcard2  6346  findcard2s  6347  ac6sfi  6352  ltbtwnnqq  6511  prnmaddl  6586  genpcdl  6615  genpcuu  6616  ltaddpr  6693  lteupri  6713  recexprlemss1l  6731  recexprlemss1u  6732  cauappcvgprlemdisj  6747  lttrsr  6845  recexgt0sr  6856  mulgt0sr  6860  axprecex  6952  rereceu  6961  recexap  7632  0mnnnnn0  8212  prime  8335  zeo  8341  fnn0ind  8352  zindd  8354  btwnz  8355  lbzbi  8549  qdenre  9772  climcau  9840  serif0  9845  bj-sbimedh  9885  bj-vtoclgft  9888  elabgft1  9891  elabgf2  9893
  Copyright terms: Public domain W3C validator