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  114  syl6ib  160  syl6ibr  161  syl6bi  162  syl6bir  163  pm5.32d  447  con2d  619  con3d  626  expi  633  pm3.37  684  pm5.21ndd  700  pm2.37  800  pm2.81  806  dcim  836  condcOLD  849  con4biddc  852  pm2.54dc  886  pm4.79dc  898  pm2.85dc  900  pm3.12dc  953  dn1dc  955  3jao  1296  xoranor  1372  syl6an  1427  syl10  1428  hbald  1484  ax12  1505  hbimd  1566  nfal  1569  19.21ht  1574  19.30dc  1620  19.23t  1670  hbexd  1687  spimth  1728  spimed  1733  cbv2h  1741  cbv2w  1743  equvini  1751  sbiedh  1780  sbcof2  1803  aev  1805  sb3  1824  hbsb2  1829  sbequilem  1831  sbft  1841  sbi1v  1884  cbvexdh  1919  nf5-1  2017  mo23  2060  moexexdc  2103  euexex  2104  exists2  2116  dvelimdc  2333  rsp2  2520  rgen2a  2524  spcimgft  2806  spcimegft  2808  eueq3dc  2904  moeq3dc  2906  reu6  2919  ssddif  3361  reupick2  3413  sssnm  3739  prneimg  3759  dfiun2g  3903  exmidsssnc  4187  exmidundifim  4191  opth1  4219  copsexg  4227  opelopabt  4245  issod  4302  sowlin  4303  suctr  4404  reusv3i  4442  ralxfrALT  4450  ssorduni  4469  onintonm  4499  regexmidlem1  4515  nlimsucg  4548  0elnn  4601  issref  4991  iotaval  5169  fun11iun  5461  brprcneu  5487  fvssunirng  5509  relfvssunirn  5510  fv3  5517  ndmfvg  5525  ssimaex  5555  fvopab3ig  5568  dff4im  5639  ffnfv  5651  fconstfvm  5711  f1mpt  5747  oprabid  5882  mpoeq123  5909  f1o2ndf1  6204  brtposg  6230  rntpos  6233  dftpos4  6239  smores2  6270  tfri3  6343  rdgss  6359  nntri3or  6469  nndifsnid  6483  nnawordex  6504  eroveu  6600  map0g  6662  fundmen  6780  nneneq  6831  fiintim  6902  snon0  6909  fnfi  6910  infnlbti  6999  exmidonfinlem  7157  exmidontri2or  7207  addclpi  7276  enq0tr  7383  genprndl  7470  genprndu  7471  genpdisj  7472  addlocprlem  7484  nqprloc  7494  recexprlemss1l  7584  recexprlemss1u  7585  suplocexprlemss  7664  elrealeu  7778  ltleletr  7988  negf1o  8288  zletric  9243  zlelttric  9244  zltnle  9245  zmulcl  9252  zdcle  9275  zdclt  9276  zeo  9304  uz11  9496  indstr  9539  eqreznegel  9560  negm  9561  lbzbi  9562  fzdcel  9983  fzm1  10043  qletric  10187  qlelttric  10188  qltnle  10189  frecuzrdgtcl  10355  frecuzrdgfunlem  10362  qsqeqor  10573  rennim  10953  maxleast  11164  negfi  11178  fsum3cvg  11328  fproddccvg  11522  prodmodc  11528  ndvdssub  11876  algcvgblem  11990  algcvga  11992  isprm3  12059  oddprmdvds  12293  4sqlem2  12328  epttop  12843  cnptoprest  12992  txcnp  13024  metequiv2  13249  cnlimcim  13393  bj-hbalt  13757  bj-intabssel1  13784  decidin  13791  sumdc2  13793  bj-charfunr  13805  bj-axemptylem  13887  bj-nnen2lp  13949  bj-nnord  13953  setindft  13960  bj-inf2vnlem2  13966  bj-inf2vnlem3  13967  bj-inf2vnlem4  13968  exmidsbthrlem  14014  triap  14021  tridceq  14048