Theorem syl6com 38

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 36	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	com12 33	1 ⊢ (𝜓 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  19.33b  1918  19.36imv  1978  sbequ2  2286  nfeqf2  2408  ax6e  2414  axc16i  2467  mo4  2593  rgen2a  3358  sbccomlem  3820  rspn0  4307  wefrc  5653  elinxp  6016  sorpssuni  7737  sorpssint  7738  ordzsl  7845  limuni3  7852  funcnvuni  7933  funrnex  7955  soxp  8131  frrlem4  8292  oaabs  8640  eceqoveq  8826  pssinf  9236  unbnn2  9271  inf0  9604  inf3lem5  9615  tcel  9726  frmin  9735  rankxpsuc  9868  carduni  9990  prdom2  10013  dfac5  10135  cflm  10255  indpi  10920  prlem934  11046  negf1o  11672  xrub  13368  injresinjlem  13850  hashgt12el  14491  hashgt12el2  14492  fi1uzind  14576  swrdwrdsymb  14736  cshwcsh2id  14903  cshwshash  17202  lidrididd  18770  dfgrp2  19092  symgextf1  19554  rngdi  20301  rngdir  20302  gsummoncoe1  22539  basis2  23182  fbdmn0  24066  rusgr1vtxlem  30055  upgrewlkle2  30074  clwwlknun  30590  conngrv2edg  30683  frcond1  30754  4cyclusnfrgr  30780  atcv0eq  32868  dfon2lem9  36376  altopthsn  36549  rankeq1o  36759  wl-orel12  38282  wl-equsb4  38328  rngoueqz  38698  hbtlem5  43977  ntrk0kbimka  44887  funressnfv  47939  afvco2  48072  ndmaovcl  48099  bgoldbtbndlem4  48732  isubgr3stgrlem4  48893  zlmodzxznm  49435