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  4144  csbexga  4161  copsexg  4277  trssord  4415  trsuc  4457  trsucss  4458  abnexg  4481  ralxfrd  4497  rexxfrd  4498  ralxfrALT  4502  sucprcreg  4585  nlimsucg  4602  tfis  4619  relssres  4984  issref  5052  dmsnopg  5141  dfco2a  5170  imadif  5338  fvelima  5612  mptfvex  5647  fvmptdf  5649  fvmptf  5654  funfvima2  5795  funfvima3  5796  foco2  5800  isores3  5862  oprabid  5954  ovmpt4g  6045  ovmpos  6046  ov2gf  6047  ovmpodf  6054  suppssfv  6131  suppssov1  6132  fo2ndf  6285  rntpos  6315  tposf2  6326  nnmordi  6574  nnmord  6575  nnaordex  6586  ectocld  6660  qsel  6671  mapsn  6749  f1oeng  6816  mapen  6907  nneneq  6918  findcard2  6950  findcard2s  6951  ac6sfi  6959  fiintim  6992  sbthlem1  7023  pr2ne  7259  ltbtwnnqq  7482  prnmaddl  7557  genpcdl  7586  genpcuu  7587  ltaddpr  7664  lteupri  7684  recexprlemss1l  7702  recexprlemss1u  7703  cauappcvgprlemdisj  7718  lttrsr  7829  recexgt0sr  7840  mulgt0sr  7845  axprecex  7947  rereceu  7956  addlsub  8396  recexap  8680  0mnnnnn0  9281  prime  9425  zeo  9431  fnn0ind  9442  zindd  9444  btwnz  9445  lbzbi  9690  addmodlteq  10490  facwordi  10832  seq3coll  10934  qdenre  11367  climcau  11512  serf0  11517  zsumdc  11549  fsum2dlemstep  11599  fsum2d  11600  fsumabs  11630  fsumiun  11642  zproddc  11744  fprod2dlemstep  11787  fprod2d  11788  odd2np1  12038  ndvdssub  12095  dfgcd2  12181  nprm  12291  rpexp  12321  pc2dvds  12499  pcfac  12519  4sqlem12  12571  4sqlem17  12576  divsfval  12971  mulgaddcom  13276  mulginvcom  13277  ringinvnz1ne0  13605  lmss  14482  lmtopcnp  14486  txcn  14511  txlm  14515  xmettri2  14597  blin2  14668  metcnp3  14747  limcresi  14902  dvmptfsum  14961  logbgcd1irr  15203  lgsdir2lem2  15270  lgsne0  15279  2lgsoddprm  15354  2sqlem6  15361  2sqlem10  15366  bj-stim  15392  bj-stan  15393  bj-stand  15394  bj-stal  15395  bj-sbimedh  15417  bj-vtoclgft  15421  elabgft1  15424  elabgf2  15426