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  3745  ssprsseq  4752  elpr2elpr  4793  disjxiun  5056  oprabidw  7181  oprabid  7182  elovmporab  7385  elovmporab1w  7386  elovmporab1  7387  mpoxopoveqd  7881  wfr3g  7947  oewordri  8212  fsuppunbi  8848  r1sdom  9197  updjud  9357  pr2ne  9425  kmlem4  9573  kmlem12  9581  domtriomlem  9858  zorn2lem6  9917  axdclem  9935  wunr1om  10135  tskr1om  10183  zindd  12077  hash2pwpr  13828  fi1uzind  13849  swrdnd0  14013  pfxccatin12  14089  repsdf2  14134  2cshwcshw  14181  cshwcshid  14183  fprodmodd  15345  alzdvds  15664  pwp1fsum  15736  lcmfdvds  15980  prm23ge5  16146  cshwshashlem2  16424  0ringnnzr  20036  01eq0ring  20039  mplcoe5lem  20242  gsummoncoe1  20466  psgndiflemA  20739  gsummatr01lem3  21260  mp2pm2mplem4  21411  fiinopn  21503  cnmptcom  22280  fgcl  22480  fmfnfmlem1  22556  fmco  22563  flffbas  22597  cnpflf2  22602  metcnp3  23144  tngngp3  23259  clmvscom  23688  cphsscph  23848  aalioulem2  24916  elntg2  26765  ausgrusgrb  26944  usgredg4  26993  nbgr1vtx  27134  uhgr0edg0rgrb  27350  uhgrwkspth  27530  usgr2wlkspth  27534  uspgrn2crct  27580  crctcshwlkn0  27593  wwlksnredwwlkn  27667  wwlksnextsurj  27672  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  frgrnbnb  28066  frgrwopreglem5  28094  frgrwopreglem5ALT  28095  cvati  30137  dmdbr5ati  30193  loop1cycl  32379  sat1el2xp  32621  dfon2lem3  33025  frr3g  33116  bj-peircestab  33883  bj-0int  34387  ptrecube  34886  fzmul  35010  zerdivemp1x  35219  psshepw  40127  ndmaovdistr  43399  ssfz12  43507  fzopredsuc  43516  smonoord  43524  elsetpreimafvbi  43544  iccpartltu  43578  iccpartgtl  43579  ichreuopeq  43628  elsprel  43630  lighneallem3  43765  odd2prm2  43876  nnsum4primeseven  43958  nnsum4primesevenALTV  43959  bgoldbnnsum3prm  43962  ringcbasbas  44298  ringcbasbasALTV  44322  ply1mulgsumlem2  44434  ldepsnlinclem1  44553  ldepsnlinclem2  44554  nnolog2flm1  44643  blengt1fldiv2p1  44646