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  8660  recexap  8945  0mnnnnn0  9548  prime  9698  zeo  9704  fnn0ind  9715  zindd  9717  btwnz  9718  lbzbi  9969  addmodlteq  10787  facwordi  11130  seq3coll  11242  ccatalpha  11329  pfxccatin12lem2a  11447  qdenre  11916  climcau  12061  serf0  12066  zsumdc  12099  fsum2dlemstep  12149  fsum2d  12150  fsumabs  12180  fsumiun  12192  zproddc  12294  fprod2dlemstep  12337  fprod2d  12338  odd2np1  12588  ndvdssub  12645  bitsinv1lem  12676  dfgcd2  12739  nprm  12849  rpexp  12879  pc2dvds  13057  pcfac  13077  4sqlem12  13129  4sqlem17  13134  divsfval  13596  mulgaddcom  13903  mulginvcom  13904  ringinvnz1ne0  14296  lmss  15241  lmtopcnp  15245  txcn  15270  txlm  15274  xmettri2  15356  blin2  15427  metcnp3  15506  limcresi  15661  dvmptfsum  15720  logbgcd1irr  15962  lgsdir2lem2  16032  lgsne0  16041  2lgsoddprm  16116  2sqlem6  16123  2sqlem10  16128  uhgr0vb  16209  wlk1walkdom  16484  wlkv0  16494  wlklenvclwlk  16498  bj-stim  16658  bj-stan  16659  bj-stand  16660  bj-stal  16661  bj-sbimedh  16683  bj-vtoclgft  16687  elabgft1  16690  elabgf2  16692