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  650  pm2.36  805  pm4.72  828  pm2.18dc  856  con1dc  857  jadc  864  pm2.521dcALT  871  con1biimdc  874  condandc  882  pm5.18dc  884  pm2.68dc  895  syl3an2  1283  syl2an23an  1310  xor3dc  1398  alrimdh  1490  spsd  1549  a5i  1554  19.21h  1568  hbnt  1664  hbae  1729  sbiedh  1798  exdistrfor  1811  sbcof2  1821  ax11a2  1832  ax11v  1838  sb4  1843  hbsb4t  2029  exmoeudc  2105  euimmo  2109  mopick  2120  r19.37  2646  spcimgft  2836  spcimegft  2838  rr19.28v  2900  mob2  2940  euind  2947  reuind  2965  sbeqalb  3042  triun  4140  csbexga  4157  copsexg  4273  trssord  4411  trsuc  4453  trsucss  4454  abnexg  4477  ralxfrd  4493  rexxfrd  4494  ralxfrALT  4498  sucprcreg  4581  nlimsucg  4598  tfis  4615  relssres  4980  issref  5048  dmsnopg  5137  dfco2a  5166  imadif  5334  fvelima  5608  mptfvex  5643  fvmptdf  5645  fvmptf  5650  funfvima2  5791  funfvima3  5792  foco2  5796  isores3  5858  oprabid  5950  ovmpt4g  6041  ovmpos  6042  ov2gf  6043  ovmpodf  6050  suppssfv  6126  suppssov1  6127  fo2ndf  6280  rntpos  6310  tposf2  6321  nnmordi  6569  nnmord  6570  nnaordex  6581  ectocld  6655  qsel  6666  mapsn  6744  f1oeng  6811  mapen  6902  nneneq  6913  findcard2  6945  findcard2s  6946  ac6sfi  6954  fiintim  6985  sbthlem1  7016  pr2ne  7252  ltbtwnnqq  7475  prnmaddl  7550  genpcdl  7579  genpcuu  7580  ltaddpr  7657  lteupri  7677  recexprlemss1l  7695  recexprlemss1u  7696  cauappcvgprlemdisj  7711  lttrsr  7822  recexgt0sr  7833  mulgt0sr  7838  axprecex  7940  rereceu  7949  addlsub  8389  recexap  8672  0mnnnnn0  9272  prime  9416  zeo  9422  fnn0ind  9433  zindd  9435  btwnz  9436  lbzbi  9681  addmodlteq  10469  facwordi  10811  seq3coll  10913  qdenre  11346  climcau  11490  serf0  11495  zsumdc  11527  fsum2dlemstep  11577  fsum2d  11578  fsumabs  11608  fsumiun  11620  zproddc  11722  fprod2dlemstep  11765  fprod2d  11766  odd2np1  12014  ndvdssub  12071  dfgcd2  12151  nprm  12261  rpexp  12291  pc2dvds  12468  pcfac  12488  4sqlem12  12540  4sqlem17  12545  divsfval  12911  mulgaddcom  13216  mulginvcom  13217  ringinvnz1ne0  13545  lmss  14414  lmtopcnp  14418  txcn  14443  txlm  14447  xmettri2  14529  blin2  14600  metcnp3  14679  limcresi  14820  logbgcd1irr  15099  lgsdir2lem2  15145  lgsne0  15154  2sqlem6  15207  2sqlem10  15212  bj-stim  15238  bj-stan  15239  bj-stand  15240  bj-stal  15241  bj-sbimedh  15263  bj-vtoclgft  15267  elabgft1  15270  elabgf2  15272