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  654  pm2.36  811  pm4.72  834  pm2.18dc  862  con1dc  863  jadc  870  pm2.521dcALT  877  con1biimdc  880  condandc  888  pm5.18dc  890  pm2.68dc  901  syl3an2  1307  syl2an23an  1335  xor3dc  1431  alrimdh  1527  spsd  1586  a5i  1591  19.21h  1605  hbnt  1701  hbae  1766  sbiedh  1835  exdistrfor  1848  sbcof2  1858  ax11a2  1869  ax11v  1875  sb4  1880  hbsb4t  2066  exmoeudc  2143  euimmo  2147  mopick  2158  r19.37  2685  spcimgft  2882  spcimegft  2884  rr19.28v  2946  mob2  2986  euind  2993  reuind  3011  sbeqalb  3088  triun  4200  csbexga  4217  copsexg  4336  trssord  4477  trsuc  4519  trsucss  4520  abnexg  4543  ralxfrd  4559  rexxfrd  4560  ralxfrALT  4564  sucprcreg  4647  nlimsucg  4664  tfis  4681  relssres  5051  issref  5119  dmsnopg  5208  dfco2a  5237  imadif  5410  fvelima  5697  mptfvex  5732  fvmptdf  5734  fvmptf  5739  funfvima2  5887  funfvima3  5888  foco2  5894  isores3  5956  oprabid  6050  ovmpt4g  6144  ovmpos  6145  ov2gf  6146  ovmpodf  6153  suppssfv  6231  suppssov1  6232  fo2ndf  6392  rntpos  6423  tposf2  6434  nnmordi  6684  nnmord  6685  nnaordex  6696  ectocld  6770  qsel  6781  mapsn  6859  f1oeng  6930  mapen  7032  nneneq  7043  findcard2  7078  findcard2s  7079  ac6sfi  7087  fiintim  7123  sbthlem1  7156  pr2ne  7397  ltbtwnnqq  7635  prnmaddl  7710  genpcdl  7739  genpcuu  7740  ltaddpr  7817  lteupri  7837  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemdisj  7871  lttrsr  7982  recexgt0sr  7993  mulgt0sr  7998  axprecex  8100  rereceu  8109  addlsub  8549  recexap  8833  0mnnnnn0  9434  prime  9579  zeo  9585  fnn0ind  9596  zindd  9598  btwnz  9599  lbzbi  9850  addmodlteq  10661  facwordi  11003  seq3coll  11107  ccatalpha  11194  pfxccatin12lem2a  11312  qdenre  11767  climcau  11912  serf0  11917  zsumdc  11950  fsum2dlemstep  12000  fsum2d  12001  fsumabs  12031  fsumiun  12043  zproddc  12145  fprod2dlemstep  12188  fprod2d  12189  odd2np1  12439  ndvdssub  12496  bitsinv1lem  12527  dfgcd2  12590  nprm  12700  rpexp  12730  pc2dvds  12908  pcfac  12928  4sqlem12  12980  4sqlem17  12985  divsfval  13416  mulgaddcom  13738  mulginvcom  13739  ringinvnz1ne0  14068  lmss  14976  lmtopcnp  14980  txcn  15005  txlm  15009  xmettri2  15091  blin2  15162  metcnp3  15241  limcresi  15396  dvmptfsum  15455  logbgcd1irr  15697  lgsdir2lem2  15764  lgsne0  15773  2lgsoddprm  15848  2sqlem6  15855  2sqlem10  15860  uhgr0vb  15941  wlk1walkdom  16216  wlkv0  16226  wlklenvclwlk  16230  bj-stim  16368  bj-stan  16369  bj-stand  16370  bj-stal  16371  bj-sbimedh  16393  bj-vtoclgft  16397  elabgft1  16400  elabgf2  16402