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  7736  sorpssint  7737  ordzsl  7844  limuni3  7851  funcnvuni  7932  funrnex  7954  soxp  8130  frrlem4  8291  oaabs  8639  eceqoveq  8825  pssinf  9235  unbnn2  9270  inf0  9603  inf3lem5  9614  tcel  9725  frmin  9734  rankxpsuc  9867  carduni  9989  prdom2  10012  dfac5  10134  cflm  10254  indpi  10919  prlem934  11045  negf1o  11671  xrub  13366  injresinjlem  13848  hashgt12el  14489  hashgt12el2  14490  fi1uzind  14574  swrdwrdsymb  14734  cshwcsh2id  14901  cshwshash  17200  lidrididd  18768  dfgrp2  19090  symgextf1  19552  rngdi  20299  rngdir  20300  gsummoncoe1  22537  basis2  23180  fbdmn0  24064  rusgr1vtxlem  30048  upgrewlkle2  30067  clwwlknun  30583  conngrv2edg  30676  frcond1  30747  4cyclusnfrgr  30773  atcv0eq  32861  dfon2lem9  36370  altopthsn  36543  rankeq1o  36753  wl-orel12  38276  wl-equsb4  38322  rngoueqz  38692  hbtlem5  43971  ntrk0kbimka  44881  funressnfv  47933  afvco2  48066  ndmaovcl  48093  bgoldbtbndlem4  48726  isubgr3stgrlem4  48887  zlmodzxznm  49429