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  658  pm2.36  816  pm4.72  839  pm2.18dc  867  con1dc  868  jadc  875  pm2.521dcALT  882  con1biimdc  885  condandc  893  pm5.18dc  895  pm2.68dc  906  syl3an2  1312  syl2an23an  1340  xor3dc  1436  alrimdh  1532  spsd  1591  a5i  1596  19.21h  1610  hbnt  1705  hbae  1770  sbiedh  1840  exdistrfor  1853  sbcof2  1863  ax11a2  1874  ax11v  1880  sb4  1885  hbsb4t  2073  exmoeudc  2150  euimmo  2154  mopick  2165  r19.37  2703  spcimgft  2901  spcimegft  2903  rr19.28v  2966  mob2  3006  euind  3013  reuind  3031  sbeqalb  3108  triun  4240  csbexga  4259  copsexg  4382  trssord  4523  trsuc  4565  trsucss  4566  abnexg  4590  ralxfrd  4606  rexxfrd  4607  ralxfrALT  4611  sucprcreg  4694  nlimsucg  4711  tfis  4728  relssres  5099  issref  5168  dmsnopg  5257  dfco2a  5286  imadif  5459  fvelima  5751  mptfvex  5788  fvmptdf  5790  fvmptf  5795  funfvima2  5945  funfvima3  5946  foco2  5953  isores3  6015  oprabid  6111  ovmpt4g  6205  ovmpos  6206  ov2gf  6207  ovmpodf  6214  suppssov1  6293  fo2ndf  6457  suppssfvg  6497  rntpos  6522  tposf2  6533  nnmordi  6783  nnmord  6784  nnaordex  6795  ectocld  6869  qsel  6880  mapsn  6966  f1oeng  7037  mapen  7140  nneneq  7152  findcard2  7187  findcard2s  7188  ac6sfi  7196  fiintim  7232  sbthlem1  7268  pr2ne  7532  ltbtwnnqq  7776  prnmaddl  7851  genpcdl  7880  genpcuu  7881  ltaddpr  7958  lteupri  7978  recexprlemss1l  7996  recexprlemss1u  7997  cauappcvgprlemdisj  8012  lttrsr  8123  recexgt0sr  8134  mulgt0sr  8139  axprecex  8241  rereceu  8250  addlsub  8690  recexap  8975  0mnnnnn0  9578  prime  9728  zeo  9734  fnn0ind  9745  zindd  9747  btwnz  9748  lbzbi  9999  addmodlteq  10818  facwordi  11161  seq3coll  11277  ccatalpha  11364  pfxccatin12lem2a  11482  qdenre  11951  climcau  12096  serf0  12101  zsumdc  12134  fsum2dlemstep  12184  fsum2d  12185  fsumabs  12215  fsumiun  12227  zproddc  12329  fprod2dlemstep  12372  fprod2d  12373  odd2np1  12623  ndvdssub  12680  bitsinv1lem  12711  dfgcd2  12774  nprm  12884  rpexp  12914  pc2dvds  13092  pcfac  13112  4sqlem12  13164  4sqlem17  13169  divsfval  13632  mulgaddcom  13932  mulginvcom  13933  ringinvnz1ne0  14337  lmss  15330  lmtopcnp  15334  txcn  15359  txlm  15363  xmettri2  15445  blin2  15516  metcnp3  15595  limcresi  15750  dvmptfsum  15809  logbgcd1irr  16052  lgsdir2lem2  16131  lgsne0  16140  2lgsoddprm  16215  2sqlem6  16222  2sqlem10  16227  uhgr0vb  16308  wlk1walkdom  16583  wlkv0  16593  wlklenvclwlk  16597  bj-stim  16757  bj-stan  16758  bj-stand  16759  bj-stal  16760  bj-sbimedh  16782  bj-vtoclgft  16786  elabgft1  16789  elabgf2  16791