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  652  pm2.36  809  pm4.72  832  pm2.18dc  860  con1dc  861  jadc  868  pm2.521dcALT  875  con1biimdc  878  condandc  886  pm5.18dc  888  pm2.68dc  899  syl3an2  1305  syl2an23an  1333  xor3dc  1429  alrimdh  1525  spsd  1584  a5i  1589  19.21h  1603  hbnt  1699  hbae  1764  sbiedh  1833  exdistrfor  1846  sbcof2  1856  ax11a2  1867  ax11v  1873  sb4  1878  hbsb4t  2064  exmoeudc  2141  euimmo  2145  mopick  2156  r19.37  2683  spcimgft  2880  spcimegft  2882  rr19.28v  2944  mob2  2984  euind  2991  reuind  3009  sbeqalb  3086  triun  4198  csbexga  4215  copsexg  4334  trssord  4475  trsuc  4517  trsucss  4518  abnexg  4541  ralxfrd  4557  rexxfrd  4558  ralxfrALT  4562  sucprcreg  4645  nlimsucg  4662  tfis  4679  relssres  5049  issref  5117  dmsnopg  5206  dfco2a  5235  imadif  5407  fvelima  5693  mptfvex  5728  fvmptdf  5730  fvmptf  5735  funfvima2  5882  funfvima3  5883  foco2  5889  isores3  5951  oprabid  6045  ovmpt4g  6139  ovmpos  6140  ov2gf  6141  ovmpodf  6148  suppssfv  6226  suppssov1  6227  fo2ndf  6387  rntpos  6418  tposf2  6429  nnmordi  6679  nnmord  6680  nnaordex  6691  ectocld  6765  qsel  6776  mapsn  6854  f1oeng  6925  mapen  7027  nneneq  7038  findcard2  7073  findcard2s  7074  ac6sfi  7082  fiintim  7118  sbthlem1  7150  pr2ne  7391  ltbtwnnqq  7628  prnmaddl  7703  genpcdl  7732  genpcuu  7733  ltaddpr  7810  lteupri  7830  recexprlemss1l  7848  recexprlemss1u  7849  cauappcvgprlemdisj  7864  lttrsr  7975  recexgt0sr  7986  mulgt0sr  7991  axprecex  8093  rereceu  8102  addlsub  8542  recexap  8826  0mnnnnn0  9427  prime  9572  zeo  9578  fnn0ind  9589  zindd  9591  btwnz  9592  lbzbi  9843  addmodlteq  10653  facwordi  10995  seq3coll  11099  ccatalpha  11183  pfxccatin12lem2a  11301  qdenre  11756  climcau  11901  serf0  11906  zsumdc  11938  fsum2dlemstep  11988  fsum2d  11989  fsumabs  12019  fsumiun  12031  zproddc  12133  fprod2dlemstep  12176  fprod2d  12177  odd2np1  12427  ndvdssub  12484  bitsinv1lem  12515  dfgcd2  12578  nprm  12688  rpexp  12718  pc2dvds  12896  pcfac  12916  4sqlem12  12968  4sqlem17  12973  divsfval  13404  mulgaddcom  13726  mulginvcom  13727  ringinvnz1ne0  14055  lmss  14963  lmtopcnp  14967  txcn  14992  txlm  14996  xmettri2  15078  blin2  15149  metcnp3  15228  limcresi  15383  dvmptfsum  15442  logbgcd1irr  15684  lgsdir2lem2  15751  lgsne0  15760  2lgsoddprm  15835  2sqlem6  15842  2sqlem10  15847  uhgr0vb  15928  wlk1walkdom  16170  wlkv0  16180  wlklenvclwlk  16184  bj-stim  16292  bj-stan  16293  bj-stand  16294  bj-stal  16295  bj-sbimedh  16317  bj-vtoclgft  16321  elabgft1  16324  elabgf2  16326