ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5 GIF 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 (𝜑𝜓)
syl5.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5 (𝜒 → (𝜑𝜃))

Proof of Theorem syl5
StepHypRef Expression
1 syl5.1 . . 3 (𝜑𝜓)
2 syl5.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5com 29 . 2 (𝜑 → (𝜒𝜃))
43com12 30 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  34  syl2im  38  imim12i  58  pm2.86d  98  syl5bi  150  syl5bir  151  syl5ib  152  adantld  272  adantrd  273  impel  274  mpan9  275  nsyli  611  pm2.36  751  pm4.72  770  pm2.18dc  784  con1dc  787  jadc  794  pm2.521dc  798  con1biimdc  801  condandc  809  pm5.18dc  811  pm2.68dc  827  annimdc  879  syl3an2  1204  syl2an23an  1231  xor3dc  1319  alrimdh  1409  spsd  1472  a5i  1476  19.21h  1490  hbnt  1584  hbae  1648  sbiedh  1712  exdistrfor  1723  sbcof2  1733  ax11a2  1744  ax11v  1750  sb4  1755  hbsb4t  1932  exmoeudc  2006  euimmo  2010  mopick  2021  r19.37  2511  spcimgft  2683  spcimegft  2685  rr19.28v  2742  mob2  2781  euind  2788  reuind  2804  sbeqalb  2879  triun  3908  csbexga  3926  copsexg  4027  trssord  4163  trsuc  4205  trsucss  4206  ralxfrd  4240  rexxfrd  4241  ralxfrALT  4245  sucprcreg  4320  nlimsucg  4337  tfis  4352  relssres  4696  issref  4757  dmsnopg  4842  dfco2a  4871  imadif  5030  fvelima  5277  mptfvex  5308  fvmptdf  5310  fvmptf  5315  foco2  5370  funfvima2  5443  funfvima3  5444  isores3  5506  oprabid  5588  ovmpt4g  5674  ovmpt2s  5675  ov2gf  5676  ovmpt2df  5683  suppssfv  5759  suppssov1  5760  fo2ndf  5899  rntpos  5926  tposf2  5937  nnmordi  6176  nnmord  6177  nnaordex  6187  ectocld  6259  qsel  6270  f1oeng  6325  nneneq  6413  findcard2  6445  findcard2s  6446  ac6sfi  6454  pr2ne  6572  ltbtwnnqq  6719  prnmaddl  6794  genpcdl  6823  genpcuu  6824  ltaddpr  6901  lteupri  6921  recexprlemss1l  6939  recexprlemss1u  6940  cauappcvgprlemdisj  6955  lttrsr  7053  recexgt0sr  7064  mulgt0sr  7068  axprecex  7160  rereceu  7169  addlsub  7593  recexap  7862  0mnnnnn0  8439  prime  8579  zeo  8585  fnn0ind  8596  zindd  8598  btwnz  8599  lbzbi  8834  addmodlteq  9532  facwordi  9816  qdenre  10289  climcau  10385  serif0  10390  odd2np1  10480  ndvdssub  10537  dfgcd2  10610  nprm  10712  rpexp  10739  bj-sbimedh  10842  bj-vtoclgft  10845  elabgft1  10848  elabgf2  10850
  Copyright terms: Public domain W3C validator