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-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl56  34  syl2im  38  imim12i  59  pm2.86d  99  syl5bi  151  syl5bir  152  syl5ib  153  adantld  276  adantrd  277  impel  278  mpan9  279  nsyli  639  pm2.36  794  pm4.72  813  const  838  pm2.18dc  841  con1dc  842  jadc  849  pm2.521dcALT  856  con1biimdc  859  condandc  867  pm5.18dc  869  pm2.68dc  880  annimdc  922  syl3an2  1251  syl2an23an  1278  xor3dc  1366  alrimdh  1456  spsd  1519  a5i  1523  19.21h  1537  hbnt  1632  hbae  1697  sbiedh  1761  exdistrfor  1773  sbcof2  1783  ax11a2  1794  ax11v  1800  sb4  1805  hbsb4t  1989  exmoeudc  2063  euimmo  2067  mopick  2078  r19.37  2586  spcimgft  2765  spcimegft  2767  rr19.28v  2827  mob2  2867  euind  2874  reuind  2892  sbeqalb  2968  triun  4046  csbexga  4063  copsexg  4173  trssord  4309  trsuc  4351  trsucss  4352  abnexg  4374  ralxfrd  4390  rexxfrd  4391  ralxfrALT  4395  sucprcreg  4471  nlimsucg  4488  tfis  4504  relssres  4864  issref  4928  dmsnopg  5017  dfco2a  5046  imadif  5210  fvelima  5480  mptfvex  5513  fvmptdf  5515  fvmptf  5520  funfvima2  5657  funfvima3  5658  foco2  5662  isores3  5723  oprabid  5810  ovmpt4g  5900  ovmpos  5901  ov2gf  5902  ovmpodf  5909  suppssfv  5985  suppssov1  5986  fo2ndf  6131  rntpos  6161  tposf2  6172  nnmordi  6419  nnmord  6420  nnaordex  6430  ectocld  6502  qsel  6513  mapsn  6591  f1oeng  6658  mapen  6747  nneneq  6758  findcard2  6790  findcard2s  6791  ac6sfi  6799  fiintim  6824  sbthlem1  6852  pr2ne  7064  ltbtwnnqq  7246  prnmaddl  7321  genpcdl  7350  genpcuu  7351  ltaddpr  7428  lteupri  7448  recexprlemss1l  7466  recexprlemss1u  7467  cauappcvgprlemdisj  7482  lttrsr  7593  recexgt0sr  7604  mulgt0sr  7609  axprecex  7711  rereceu  7720  addlsub  8155  recexap  8437  0mnnnnn0  9032  prime  9173  zeo  9179  fnn0ind  9190  zindd  9192  btwnz  9193  lbzbi  9434  addmodlteq  10201  facwordi  10517  seq3coll  10616  qdenre  11005  climcau  11147  serf0  11152  zsumdc  11184  fsum2dlemstep  11234  fsum2d  11235  fsumabs  11265  fsumiun  11277  zproddc  11379  odd2np1  11604  ndvdssub  11661  dfgcd2  11736  nprm  11838  rpexp  11865  lmss  12452  lmtopcnp  12456  txcn  12481  txlm  12485  xmettri2  12567  blin2  12638  metcnp3  12717  limcresi  12841  logbgcd1irr  13090  bj-stim  13123  bj-stan  13124  bj-stand  13125  bj-stal  13126  bj-sbimedh  13147  bj-vtoclgft  13151  elabgft1  13154  elabgf2  13156
  Copyright terms: Public domain W3C validator