ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5 Structured version   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  565  pm2.36  704  pm4.72  724  pm2.18dc  741  con1dc  746  jadc  753  pm2.521dc  757  con1biimdc  760  condandc  768  pm5.18dc  770  pm2.68dc  786  annimdc  833  syl3an2  1155  xor3dc  1261  alrimdh  1348  spsd  1413  a5i  1417  19.21h  1431  hbnt  1525  hbae  1588  sbiedh  1652  exdistrfor  1663  sbcof2  1673  ax11a2  1684  ax11v  1690  sb4  1695  hbsb4t  1871  exmoeudc  1945  euimmo  1949  mopick  1960  r19.37  2440  spcimgft  2606  spcimegft  2608  rr19.28v  2660  mob2  2698  euind  2705  reuind  2721  sbeqalb  2792  sbcimdv  2800  triun  3841  csbexgOLD  3859  copsexg  3955  trssord  4066  trsuc  4109  trsucss  4110  ralxfrd  4144  rexxfrd  4145  ralxfrALT  4149  sucprcreg  4211  nlimsucg  4226  tfis  4233  relssres  4575  issref  4634  dmsnopg  4719  dfco2a  4748  imadif  4905  fvelima  5150  mptfvex  5181  fvmptdf  5183  fvmptf  5188  foco2  5243  funfvima2  5316  funfvima3  5317  isores3  5380  oprabid  5461  ovmpt4g  5546  ovmpt2s  5547  ov2gf  5548  ovmpt2df  5555  suppssfv  5631  suppssov1  5632  fo2ndf  5771  rntpos  5794  tposf2  5805  nnmordi  6000  nnmord  6001  nnaordex  6011  ectocld  6083  qsel  6094  ltbtwnnqq  6272  prnmaddl  6344  genpcdl  6374  genpcuu  6375  ltaddpr  6434  recexprlemss1l  6469  recexprlemss1u  6470  lttrsr  6509  recexsrlem  6520  mulgt0sr  6522  axprecex  6574  bj-sbimedh  7018  bj-vtoclgft  7021  elabgft1  7024  elabgf2  7026
  Copyright terms: Public domain W3C validator