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  2879  spcimegft  2881  rr19.28v  2943  mob2  2983  euind  2990  reuind  3008  sbeqalb  3085  triun  4195  csbexga  4212  copsexg  4331  trssord  4472  trsuc  4514  trsucss  4515  abnexg  4538  ralxfrd  4554  rexxfrd  4555  ralxfrALT  4559  sucprcreg  4642  nlimsucg  4659  tfis  4676  relssres  5046  issref  5114  dmsnopg  5203  dfco2a  5232  imadif  5404  fvelima  5690  mptfvex  5725  fvmptdf  5727  fvmptf  5732  funfvima2  5879  funfvima3  5880  foco2  5886  isores3  5948  oprabid  6042  ovmpt4g  6136  ovmpos  6137  ov2gf  6138  ovmpodf  6145  suppssfv  6223  suppssov1  6224  fo2ndf  6384  rntpos  6414  tposf2  6425  nnmordi  6675  nnmord  6676  nnaordex  6687  ectocld  6761  qsel  6772  mapsn  6850  f1oeng  6921  mapen  7020  nneneq  7031  findcard2  7064  findcard2s  7065  ac6sfi  7073  fiintim  7109  sbthlem1  7140  pr2ne  7381  ltbtwnnqq  7618  prnmaddl  7693  genpcdl  7722  genpcuu  7723  ltaddpr  7800  lteupri  7820  recexprlemss1l  7838  recexprlemss1u  7839  cauappcvgprlemdisj  7854  lttrsr  7965  recexgt0sr  7976  mulgt0sr  7981  axprecex  8083  rereceu  8092  addlsub  8532  recexap  8816  0mnnnnn0  9417  prime  9562  zeo  9568  fnn0ind  9579  zindd  9581  btwnz  9582  lbzbi  9828  addmodlteq  10637  facwordi  10979  seq3coll  11082  ccatalpha  11166  pfxccatin12lem2a  11280  qdenre  11734  climcau  11879  serf0  11884  zsumdc  11916  fsum2dlemstep  11966  fsum2d  11967  fsumabs  11997  fsumiun  12009  zproddc  12111  fprod2dlemstep  12154  fprod2d  12155  odd2np1  12405  ndvdssub  12462  bitsinv1lem  12493  dfgcd2  12556  nprm  12666  rpexp  12696  pc2dvds  12874  pcfac  12894  4sqlem12  12946  4sqlem17  12951  divsfval  13382  mulgaddcom  13704  mulginvcom  13705  ringinvnz1ne0  14033  lmss  14941  lmtopcnp  14945  txcn  14970  txlm  14974  xmettri2  15056  blin2  15127  metcnp3  15206  limcresi  15361  dvmptfsum  15420  logbgcd1irr  15662  lgsdir2lem2  15729  lgsne0  15738  2lgsoddprm  15813  2sqlem6  15820  2sqlem10  15825  uhgr0vb  15905  wlk1walkdom  16131  wlkv0  16141  wlklenvclwlk  16145  bj-stim  16219  bj-stan  16220  bj-stand  16221  bj-stal  16222  bj-sbimedh  16244  bj-vtoclgft  16248  elabgft1  16251  elabgf2  16253