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:  2rmorex  3714  ssprsseq  4783  preqsnd  4817  elpr2elpr  4827  disjxiun  5097  oprabidw  7399  oprabid  7400  elovmporab  7614  elovmporab1w  7615  elovmporab1  7616  mpoxopoveqd  8173  wfr3g  8271  oewordri  8530  fsuppunbi  9304  frr3g  9680  r1sdom  9698  updjud  9858  kmlem4  10076  kmlem12  10084  domtriomlem  10364  zorn2lem6  10423  axdclem  10441  wunr1om  10642  tskr1om  10690  zindd  12605  hash2pwpr  14411  fi1uzind  14442  swrdnd0  14593  pfxccatin12  14668  repsdf2  14713  2cshwcshw  14760  cshwcshid  14762  fprodmodd  15932  alzdvds  16259  pwp1fsum  16330  lcmfdvds  16581  prm23ge5  16755  cshwshashlem2  17036  0ringnnzr  20470  01eq0ringOLD  20476  ringcbasbas  20618  psgndiflemA  21568  mplcoe5lem  22006  gsummoncoe1  22264  gsummatr01lem3  22613  mp2pm2mplem4  22765  fiinopn  22857  cnmptcom  23634  fgcl  23834  fmfnfmlem1  23910  fmco  23917  flffbas  23951  cnpflf2  23956  metcnp3  24496  tngngp3  24612  clmvscom  25058  cphsscph  25219  aalioulem2  26309  elntg2  29070  ausgrusgrb  29250  usgredg4  29302  nbgr1vtx  29443  uhgr0edg0rgrb  29660  uhgrwkspth  29840  usgr2wlkspth  29844  uspgrn2crct  29893  crctcshwlkn0  29906  wwlksnredwwlkn  29980  wwlksnextsurj  29985  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  frgrnbnb  30380  frgrwopreglem5  30408  frgrwopreglem5ALT  30409  cvati  32453  dmdbr5ati  32509  loop1cycl  35350  sat1el2xp  35592  antnest  35902  dfon2lem3  35996  bj-peircestab  36772  bj-0int  37351  ptrecube  37868  fzmul  37989  zerdivemp1x  38195  psshepw  44141  ndmaovdistr  47564  ssfz12  47671  fzopredsuc  47680  smonoord  47728  elsetpreimafvbi  47748  iccpartltu  47782  iccpartgtl  47783  ichreuopeq  47830  elsprel  47832  lighneallem3  47964  odd2prm2  48075  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  bgoldbnnsum3prm  48161  clnbgrgrimlem  48290  grtrif1o  48299  grtriclwlk3  48302  gpgprismgr4cycllem7  48458  pgnbgreunbgr  48482  ringcbasbasALTV  48669  ply1mulgsumlem2  48744  ldepsnlinclem1  48862  ldepsnlinclem2  48863  nnolog2flm1  48947  blengt1fldiv2p1  48950