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  1917  19.36imv  1977  sbequ2  2284  nfeqf2  2406  ax6e  2412  axc16i  2465  mo4  2591  rgen2a  3356  sbccomlem  3816  rspn0  4303  wefrc  5644  elinxp  6007  sorpssuni  7748  sorpssint  7749  ordzsl  7856  limuni3  7863  funcnvuni  7944  funrnex  7966  soxp  8141  frrlem4  8308  oaabs  8658  eceqoveq  8844  pssinf  9254  unbnn2  9290  inf0  9623  inf3lem5  9634  tcel  9745  frmin  9754  rankxpsuc  9900  carduni  10063  prdom2  10086  dfac5  10208  cflm  10328  indpi  10993  prlem934  11119  negf1o  11747  xrub  13443  injresinjlem  13926  hashgt12el  14568  hashgt12el2  14569  fi1uzind  14653  swrdwrdsymb  14813  cshwcsh2id  14980  cshwshash  17283  lidrididd  18852  dfgrp2  19174  symgextf1  19636  rngdi  20383  rngdir  20384  gsummoncoe1  22627  basis2  23270  fbdmn0  24154  rusgr1vtxlem  30169  upgrewlkle2  30188  clwwlknun  30704  conngrv2edg  30797  frcond1  30868  4cyclusnfrgr  30894  atcv0eq  32982  dfon2lem9  36628  altopthsn  36801  rankeq1o  37007  mh-inf3f1  37404  wl-orel12  38519  wl-equsb4  38565  rngoueqz  38950  hbtlem5  44206  ntrk0kbimka  45115  funressnfv  48189  afvco2  48322  ndmaovcl  48349  bgoldbtbndlem4  48982  isubgr3stgrlem4  49143  zlmodzxznm  49685