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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl56  34  syl2im  38  imim12i  59  pm2.86d  99  syl5bi  151  syl5bir  152  syl5ib  153  adantld  274  adantrd  275  impel  276  mpan9  277  nsyli  618  pm2.36  759  pm4.72  778  pm2.18dc  794  con1dc  797  jadc  804  pm2.521dc  808  con1biimdc  811  condandc  819  pm5.18dc  821  pm2.68dc  837  annimdc  889  syl3an2  1218  syl2an23an  1245  xor3dc  1333  alrimdh  1423  spsd  1486  a5i  1490  19.21h  1504  hbnt  1599  hbae  1664  sbiedh  1728  exdistrfor  1739  sbcof2  1749  ax11a2  1760  ax11v  1766  sb4  1771  hbsb4t  1949  exmoeudc  2023  euimmo  2027  mopick  2038  r19.37  2541  spcimgft  2717  spcimegft  2719  rr19.28v  2778  mob2  2817  euind  2824  reuind  2842  sbeqalb  2917  triun  3979  csbexga  3996  copsexg  4104  trssord  4240  trsuc  4282  trsucss  4283  abnexg  4305  ralxfrd  4321  rexxfrd  4322  ralxfrALT  4326  sucprcreg  4402  nlimsucg  4419  tfis  4435  relssres  4793  issref  4857  dmsnopg  4946  dfco2a  4975  imadif  5139  fvelima  5405  mptfvex  5438  fvmptdf  5440  fvmptf  5445  funfvima2  5582  funfvima3  5583  foco2  5587  isores3  5648  oprabid  5735  ovmpt4g  5825  ovmpos  5826  ov2gf  5827  ovmpodf  5834  suppssfv  5910  suppssov1  5911  fo2ndf  6054  rntpos  6084  tposf2  6095  nnmordi  6342  nnmord  6343  nnaordex  6353  ectocld  6425  qsel  6436  mapsn  6514  f1oeng  6581  mapen  6669  nneneq  6680  findcard2  6712  findcard2s  6713  ac6sfi  6721  fiintim  6746  sbthlem1  6773  pr2ne  6959  ltbtwnnqq  7124  prnmaddl  7199  genpcdl  7228  genpcuu  7229  ltaddpr  7306  lteupri  7326  recexprlemss1l  7344  recexprlemss1u  7345  cauappcvgprlemdisj  7360  lttrsr  7458  recexgt0sr  7469  mulgt0sr  7473  axprecex  7565  rereceu  7574  addlsub  7999  recexap  8275  0mnnnnn0  8861  prime  9002  zeo  9008  fnn0ind  9019  zindd  9021  btwnz  9022  lbzbi  9258  addmodlteq  10012  facwordi  10327  seq3coll  10426  qdenre  10814  climcau  10955  serf0  10960  zsumdc  10992  fsum2dlemstep  11042  fsum2d  11043  fsumabs  11073  fsumiun  11085  odd2np1  11365  ndvdssub  11422  dfgcd2  11495  nprm  11597  rpexp  11624  lmss  12196  lmtopcnp  12200  txcn  12225  txlm  12229  xmettri2  12289  blin2  12360  metcnp3  12435  limcresi  12515  bj-sbimedh  12560  bj-vtoclgft  12563  elabgft1  12566  elabgf2  12568