Theorem syl6 33

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)

Hypotheses

Ref	Expression
syl6.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl6.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6

Step	Hyp	Ref	Expression
1		syl6.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6.2	. . 3 ⊢ (𝜒 → 𝜃)
3	2	a1i 9	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 3	sylcom 28	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  syl6com  35  a1dd  48  syl6mpi  64  syl6c  66  com34  83  ex  115  syl6ib  161  syl6ibr  162  syl6bi  163  syl6bir  164  pm5.32d  450  con2d  624  con3d  631  expi  638  pm3.37  689  pm5.21ndd  705  pm2.37  805  pm2.81  811  dcim  841  condcOLD  854  con4biddc  857  pm2.54dc  891  pm4.79dc  903  pm2.85dc  905  pm3.12dc  958  dn1dc  960  3jao  1301  xoranor  1377  syl6an  1434  syl10  1435  hbald  1491  ax12  1512  hbimd  1573  nfal  1576  19.21ht  1581  19.30dc  1627  19.23t  1677  hbexd  1694  spimth  1735  spimed  1740  cbv2h  1748  cbv2w  1750  equvini  1758  sbiedh  1787  sbcof2  1810  aev  1812  sb3  1831  hbsb2  1836  sbequilem  1838  sbft  1848  sbi1v  1891  cbvexdh  1926  nf5-1  2024  mo23  2067  moexexdc  2110  euexex  2111  exists2  2123  dvelimdc  2340  rsp2  2527  rgen2a  2531  spcimgft  2813  spcimegft  2815  eueq3dc  2911  moeq3dc  2913  reu6  2926  ssddif  3369  reupick2  3421  sssnm  3753  prneimg  3773  dfiun2g  3917  exmidsssnc  4201  exmidundifim  4205  opth1  4234  copsexg  4242  opelopabt  4260  issod  4317  sowlin  4318  suctr  4419  reusv3i  4457  ralxfrALT  4465  ssorduni  4484  onintonm  4514  regexmidlem1  4530  nlimsucg  4563  0elnn  4616  issref  5008  iotaval  5186  fun11iun  5479  brprcneu  5505  fvssunirng  5527  relfvssunirn  5528  fv3  5535  ndmfvg  5543  ssimaex  5574  fvopab3ig  5587  dff4im  5659  ffnfv  5671  fconstfvm  5731  f1mpt  5767  oprabid  5902  mpoeq123  5929  f1o2ndf1  6224  brtposg  6250  rntpos  6253  dftpos4  6259  smores2  6290  tfri3  6363  rdgss  6379  nntri3or  6489  nndifsnid  6503  nnawordex  6525  eroveu  6621  map0g  6683  fundmen  6801  nneneq  6852  fiintim  6923  snon0  6930  fnfi  6931  infnlbti  7020  exmidonfinlem  7187  exmidontri2or  7237  addclpi  7321  enq0tr  7428  genprndl  7515  genprndu  7516  genpdisj  7517  addlocprlem  7529  nqprloc  7539  recexprlemss1l  7629  recexprlemss1u  7630  suplocexprlemss  7709  elrealeu  7823  ltleletr  8033  negf1o  8333  zletric  9291  zlelttric  9292  zltnle  9293  zmulcl  9300  zdcle  9323  zdclt  9324  zeo  9352  uz11  9544  indstr  9587  eqreznegel  9608  negm  9609  lbzbi  9610  fzdcel  10033  fzm1  10093  qletric  10237  qlelttric  10238  qltnle  10239  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  qsqeqor  10623  rennim  11002  maxleast  11213  negfi  11227  fsum3cvg  11377  fproddccvg  11571  prodmodc  11577  ndvdssub  11925  algcvgblem  12039  algcvga  12041  isprm3  12108  oddprmdvds  12342  4sqlem2  12377  epttop  13372  cnptoprest  13521  txcnp  13553  metequiv2  13778  cnlimcim  13922  bj-hbalt  14286  bj-intabssel1  14313  decidin  14320  sumdc2  14322  bj-charfunr  14333  bj-axemptylem  14415  bj-nnen2lp  14477  bj-nnord  14481  setindft  14488  bj-inf2vnlem2  14494  bj-inf2vnlem3  14495  bj-inf2vnlem4  14496  exmidsbthrlem  14541  triap  14548  tridceq  14575