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  1920  19.36imv  1980  sbequ2  2288  nfeqf2  2409  ax6e  2415  axc16i  2468  mo4  2594  rgen2a  3360  sbccomlem  3821  rspn0  4307  wefrc  5649  elinxp  6020  sorpssuni  7772  sorpssint  7773  ordzsl  7880  limuni3  7887  funcnvuni  7968  funrnex  7990  soxp  8168  frrlem4  8335  oaabs  8685  eceqoveq  8871  pssinf  9281  unbnn2  9317  inf0  9649  inf3lem5  9660  tcel  9771  frmin  9780  rankxpsuc  9926  carduni  10089  prdom2  10112  dfac5  10234  cflm  10354  indpi  11019  prlem934  11145  negf1o  11773  xrub  13469  injresinjlem  13952  hashgt12el  14594  hashgt12el2  14595  fi1uzind  14679  swrdwrdsymb  14840  cshwcsh2id  15007  cshwshash  17311  lidrididd  18880  dfgrp2  19202  symgextf1  19665  rngdi  20412  rngdir  20413  gsummoncoe1  22656  basis2  23299  fbdmn0  24183  rusgr1vtxlem  30198  upgrewlkle2  30217  clwwlknun  30733  conngrv2edg  30826  frcond1  30897  4cyclusnfrgr  30923  atcv0eq  33011  dfon2lem9  36731  altopthsn  36904  rankeq1o  37110  mh-inf3f1  37507  wl-orel12  38635  wl-equsb4  38681  rngoueqz  39066  hbtlem5  44322  ntrk0kbimka  45231  funressnfv  48318  afvco2  48451  ndmaovcl  48478  bgoldbtbndlem4  49111  isubgr3stgrlem4  49272  zlmodzxznm  49814