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

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5com 29	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 30	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  100  biimtrid  152  biimtrrid  153  imbitrid  154  adantld  278  adantrd  279  impel  280  mpan9  281  nsyli  654  pm2.36  812  pm4.72  835  pm2.18dc  863  con1dc  864  jadc  871  pm2.521dcALT  878  con1biimdc  881  condandc  889  pm5.18dc  891  pm2.68dc  902  syl3an2  1308  syl2an23an  1336  xor3dc  1432  alrimdh  1528  spsd  1587  a5i  1592  19.21h  1606  hbnt  1701  hbae  1766  sbiedh  1836  exdistrfor  1849  sbcof2  1859  ax11a2  1870  ax11v  1876  sb4  1881  hbsb4t  2069  exmoeudc  2146  euimmo  2150  mopick  2161  r19.37  2697  spcimgft  2895  spcimegft  2897  rr19.28v  2960  mob2  3000  euind  3007  reuind  3025  sbeqalb  3102  triun  4226  csbexga  4243  copsexg  4365  trssord  4506  trsuc  4548  trsucss  4549  abnexg  4572  ralxfrd  4588  rexxfrd  4589  ralxfrALT  4593  sucprcreg  4676  nlimsucg  4693  tfis  4710  relssres  5081  issref  5150  dmsnopg  5239  dfco2a  5268  imadif  5441  fvelima  5733  mptfvex  5768  fvmptdf  5770  fvmptf  5775  funfvima2  5924  funfvima3  5925  foco2  5932  isores3  5994  oprabid  6090  ovmpt4g  6184  ovmpos  6185  ov2gf  6186  ovmpodf  6193  suppssov1  6272  fo2ndf  6436  suppssfvg  6476  rntpos  6501  tposf2  6512  nnmordi  6762  nnmord  6763  nnaordex  6774  ectocld  6848  qsel  6859  mapsn  6938  f1oeng  7009  mapen  7112  nneneq  7124  findcard2  7159  findcard2s  7160  ac6sfi  7168  fiintim  7204  sbthlem1  7240  pr2ne  7502  ltbtwnnqq  7746  prnmaddl  7821  genpcdl  7850  genpcuu  7851  ltaddpr  7928  lteupri  7948  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemdisj  7982  lttrsr  8093  recexgt0sr  8104  mulgt0sr  8109  axprecex  8211  rereceu  8220  addlsub  8659  recexap  8944  0mnnnnn0  9545  prime  9695  zeo  9701  fnn0ind  9712  zindd  9714  btwnz  9715  lbzbi  9966  addmodlteq  10784  facwordi  11127  seq3coll  11239  ccatalpha  11326  pfxccatin12lem2a  11444  qdenre  11912  climcau  12057  serf0  12062  zsumdc  12095  fsum2dlemstep  12145  fsum2d  12146  fsumabs  12176  fsumiun  12188  zproddc  12290  fprod2dlemstep  12333  fprod2d  12334  odd2np1  12584  ndvdssub  12641  bitsinv1lem  12672  dfgcd2  12735  nprm  12845  rpexp  12875  pc2dvds  13053  pcfac  13073  4sqlem12  13125  4sqlem17  13130  divsfval  13625  mulgaddcom  13947  mulginvcom  13948  ringinvnz1ne0  14277  lmss  15223  lmtopcnp  15227  txcn  15252  txlm  15256  xmettri2  15338  blin2  15409  metcnp3  15488  limcresi  15643  dvmptfsum  15702  logbgcd1irr  15944  lgsdir2lem2  16014  lgsne0  16023  2lgsoddprm  16098  2sqlem6  16105  2sqlem10  16110  uhgr0vb  16191  wlk1walkdom  16466  wlkv0  16476  wlklenvclwlk  16480  bj-stim  16630  bj-stan  16631  bj-stand  16632  bj-stal  16633  bj-sbimedh  16655  bj-vtoclgft  16659  elabgft1  16662  elabgf2  16664