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  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  2705  mob2  2743  euind  2750  reuind  2766  sbeqalb  2841  triun  3894  csbexga  3912  copsexg  4008  trssord  4144  trsuc  4186  trsucss  4187  ralxfrd  4221  rexxfrd  4222  ralxfrALT  4226  sucprcreg  4300  nlimsucg  4317  tfis  4333  relssres  4675  issref  4734  dmsnopg  4819  dfco2a  4848  imadif  5006  fvelima  5252  mptfvex  5283  fvmptdf  5285  fvmptf  5290  foco2  5345  funfvima2  5418  funfvima3  5419  isores3  5482  oprabid  5564  ovmpt4g  5650  ovmpt2s  5651  ov2gf  5652  ovmpt2df  5659  suppssfv  5735  suppssov1  5736  fo2ndf  5875  rntpos  5902  tposf2  5913  nnmordi  6119  nnmord  6120  nnaordex  6130  ectocld  6202  qsel  6213  f1oeng  6267  nneneq  6350  findcard2  6376  findcard2s  6377  ac6sfi  6382  ltbtwnnqq  6570  prnmaddl  6645  genpcdl  6674  genpcuu  6675  ltaddpr  6752  lteupri  6772  recexprlemss1l  6790  recexprlemss1u  6791  cauappcvgprlemdisj  6806  lttrsr  6904  recexgt0sr  6915  mulgt0sr  6919  axprecex  7011  rereceu  7020  addlsub  7439  recexap  7707  0mnnnnn0  8270  prime  8395  zeo  8401  fnn0ind  8412  zindd  8414  btwnz  8415  lbzbi  8647  addmodlteq  9342  facwordi  9601  qdenre  10021  climcau  10089  serif0  10094  odd2np1  10176  bj-sbimedh  10270  bj-vtoclgft  10273  elabgft1  10276  elabgf2  10278
  Copyright terms: Public domain W3C validator