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  1493  spsd  1552  a5i  1557  19.21h  1571  hbnt  1667  hbae  1732  sbiedh  1801  exdistrfor  1814  sbcof2  1824  ax11a2  1835  ax11v  1841  sb4  1846  hbsb4t  2032  exmoeudc  2108  euimmo  2112  mopick  2123  r19.37  2649  spcimgft  2840  spcimegft  2842  rr19.28v  2904  mob2  2944  euind  2951  reuind  2969  sbeqalb  3046  triun  4145  csbexga  4162  copsexg  4278  trssord  4416  trsuc  4458  trsucss  4459  abnexg  4482  ralxfrd  4498  rexxfrd  4499  ralxfrALT  4503  sucprcreg  4586  nlimsucg  4603  tfis  4620  relssres  4985  issref  5053  dmsnopg  5142  dfco2a  5171  imadif  5339  fvelima  5615  mptfvex  5650  fvmptdf  5652  fvmptf  5657  funfvima2  5798  funfvima3  5799  foco2  5803  isores3  5865  oprabid  5957  ovmpt4g  6049  ovmpos  6050  ov2gf  6051  ovmpodf  6058  suppssfv  6135  suppssov1  6136  fo2ndf  6294  rntpos  6324  tposf2  6335  nnmordi  6583  nnmord  6584  nnaordex  6595  ectocld  6669  qsel  6680  mapsn  6758  f1oeng  6825  mapen  6916  nneneq  6927  findcard2  6959  findcard2s  6960  ac6sfi  6968  fiintim  7001  sbthlem1  7032  pr2ne  7273  ltbtwnnqq  7501  prnmaddl  7576  genpcdl  7605  genpcuu  7606  ltaddpr  7683  lteupri  7703  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemdisj  7737  lttrsr  7848  recexgt0sr  7859  mulgt0sr  7864  axprecex  7966  rereceu  7975  addlsub  8415  recexap  8699  0mnnnnn0  9300  prime  9444  zeo  9450  fnn0ind  9461  zindd  9463  btwnz  9464  lbzbi  9709  addmodlteq  10509  facwordi  10851  seq3coll  10953  qdenre  11386  climcau  11531  serf0  11536  zsumdc  11568  fsum2dlemstep  11618  fsum2d  11619  fsumabs  11649  fsumiun  11661  zproddc  11763  fprod2dlemstep  11806  fprod2d  11807  odd2np1  12057  ndvdssub  12114  bitsinv1lem  12145  dfgcd2  12208  nprm  12318  rpexp  12348  pc2dvds  12526  pcfac  12546  4sqlem12  12598  4sqlem17  12603  divsfval  13032  mulgaddcom  13354  mulginvcom  13355  ringinvnz1ne0  13683  lmss  14590  lmtopcnp  14594  txcn  14619  txlm  14623  xmettri2  14705  blin2  14776  metcnp3  14855  limcresi  15010  dvmptfsum  15069  logbgcd1irr  15311  lgsdir2lem2  15378  lgsne0  15387  2lgsoddprm  15462  2sqlem6  15469  2sqlem10  15474  bj-stim  15500  bj-stan  15501  bj-stand  15502  bj-stal  15503  bj-sbimedh  15525  bj-vtoclgft  15529  elabgft1  15532  elabgf2  15534