Theorem syl6com 37

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem syl6com

Step	Hyp	Ref	Expression
1		syl6com.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6com.2	. . 3 ⊢ (𝜒 → 𝜃)
3	1, 2	syl6 35	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	com12 32	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:  19.33b  1886  sbequ2  2247  nfeqf2  2384  ax6e  2390  axc16i  2447  mo4  2625  rgen2a  3193  rspn0  4266  wefrc  5513  elinxp  5856  sorpssuni  7438  sorpssint  7439  ordzsl  7540  limuni3  7547  funcnvuni  7618  funrnex  7637  soxp  7806  wfrlem4  7941  wfrlem12  7949  oaabs  8254  eceqoveq  8385  php3  8687  pssinf  8712  unbnn2  8759  inf0  9068  inf3lem5  9079  tcel  9171  rankxpsuc  9295  carduni  9394  prdom2  9417  dfac5  9539  cflm  9661  indpi  10318  prlem934  10444  negf1o  11059  xrub  12693  injresinjlem  13152  hashgt12el  13779  hashgt12el2  13780  fi1uzind  13851  swrdwrdsymb  14015  cshwcsh2id  14181  cshwshash  16430  lidrididd  17872  dfgrp2  18120  symgextf1  18541  gsummoncoe1  20933  basis2  21556  fbdmn0  22439  rusgr1vtxlem  27377  upgrewlkle2  27396  clwwlknun  27897  conngrv2edg  27980  frcond1  28051  4cyclusnfrgr  28077  atcv0eq  30162  dfon2lem9  33149  trpredrec  33190  frmin  33197  frrlem4  33239  altopthsn  33535  rankeq1o  33745  bj-cbvalimt  34085  bj-cbveximt  34086  wl-orel12  34916  wl-equsb4  34958  rngoueqz  35378  hbtlem5  40072  ntrk0kbimka  40742  funressnfv  43635  afvco2  43732  ndmaovcl  43759  bgoldbtbndlem4  44326  rngdir  44506  zlmodzxznm  44906