Theorem syl11 33

Description: A syllogism inference. Commuted form of an instance of syl 17. (Contributed by BJ, 25-Oct-2021.)

Hypotheses

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

Assertion

Ref	Expression
syl11	⊢ (𝜓 → (𝜃 → 𝜒))

Proof of Theorem syl11

Step	Hyp	Ref	Expression
1		syl11.2	. . 3 ⊢ (𝜃 → 𝜑)
2		syl11.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl 17	. 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:  r19.35OLD  3089  2rmorex  3725  ssprsseq  4789  preqsnd  4823  elpr2elpr  4833  disjxiun  5104  oprabidw  7418  oprabid  7419  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  mpoxopoveqd  8200  wfr3g  8298  oewordri  8556  fsuppunbi  9340  frr3g  9709  r1sdom  9727  updjud  9887  pr2neOLD  9958  kmlem4  10107  kmlem12  10115  domtriomlem  10395  zorn2lem6  10454  axdclem  10472  wunr1om  10672  tskr1om  10720  zindd  12635  hash2pwpr  14441  fi1uzind  14472  swrdnd0  14622  pfxccatin12  14698  repsdf2  14743  2cshwcshw  14791  cshwcshid  14793  fprodmodd  15963  alzdvds  16290  pwp1fsum  16361  lcmfdvds  16612  prm23ge5  16786  cshwshashlem2  17067  0ringnnzr  20434  01eq0ringOLD  20440  ringcbasbas  20582  psgndiflemA  21510  mplcoe5lem  21946  gsummoncoe1  22195  gsummatr01lem3  22544  mp2pm2mplem4  22696  fiinopn  22788  cnmptcom  23565  fgcl  23765  fmfnfmlem1  23841  fmco  23848  flffbas  23882  cnpflf2  23887  metcnp3  24428  tngngp3  24544  clmvscom  24990  cphsscph  25151  aalioulem2  26241  elntg2  28912  ausgrusgrb  29092  usgredg4  29144  nbgr1vtx  29285  uhgr0edg0rgrb  29502  uhgrwkspth  29685  usgr2wlkspth  29689  uspgrn2crct  29738  crctcshwlkn0  29751  wwlksnredwwlkn  29825  wwlksnextsurj  29830  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  frgrnbnb  30222  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  cvati  32295  dmdbr5ati  32351  loop1cycl  35124  sat1el2xp  35366  antnest  35676  dfon2lem3  35773  bj-peircestab  36541  bj-0int  37089  ptrecube  37614  fzmul  37735  zerdivemp1x  37941  psshepw  43777  ndmaovdistr  47208  ssfz12  47315  fzopredsuc  47324  smonoord  47372  elsetpreimafvbi  47392  iccpartltu  47426  iccpartgtl  47427  ichreuopeq  47474  elsprel  47476  lighneallem3  47608  odd2prm2  47719  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbnnsum3prm  47805  clnbgrgrimlem  47933  grtrif1o  47941  grtriclwlk3  47944  gpgprismgr4cycllem7  48091  pgnbgreunbgr  48115  ringcbasbasALTV  48300  ply1mulgsumlem2  48376  ldepsnlinclem1  48494  ldepsnlinclem2  48495  nnolog2flm1  48579  blengt1fldiv2p1  48582