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  3712  ssprsseq  4781  preqsnd  4815  elpr2elpr  4825  disjxiun  5095  oprabidw  7389  oprabid  7390  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  mpoxopoveqd  8163  wfr3g  8261  oewordri  8520  fsuppunbi  9292  frr3g  9668  r1sdom  9686  updjud  9846  kmlem4  10064  kmlem12  10072  domtriomlem  10352  zorn2lem6  10411  axdclem  10429  wunr1om  10630  tskr1om  10678  zindd  12593  hash2pwpr  14399  fi1uzind  14430  swrdnd0  14581  pfxccatin12  14656  repsdf2  14701  2cshwcshw  14748  cshwcshid  14750  fprodmodd  15920  alzdvds  16247  pwp1fsum  16318  lcmfdvds  16569  prm23ge5  16743  cshwshashlem2  17024  0ringnnzr  20458  01eq0ringOLD  20464  ringcbasbas  20606  psgndiflemA  21556  mplcoe5lem  21994  gsummoncoe1  22252  gsummatr01lem3  22601  mp2pm2mplem4  22753  fiinopn  22845  cnmptcom  23622  fgcl  23822  fmfnfmlem1  23898  fmco  23905  flffbas  23939  cnpflf2  23944  metcnp3  24484  tngngp3  24600  clmvscom  25046  cphsscph  25207  aalioulem2  26297  elntg2  29058  ausgrusgrb  29238  usgredg4  29290  nbgr1vtx  29431  uhgr0edg0rgrb  29648  uhgrwkspth  29828  usgr2wlkspth  29832  uspgrn2crct  29881  crctcshwlkn0  29894  wwlksnredwwlkn  29968  wwlksnextsurj  29973  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  frgrnbnb  30368  frgrwopreglem5  30396  frgrwopreglem5ALT  30397  cvati  32441  dmdbr5ati  32497  loop1cycl  35331  sat1el2xp  35573  antnest  35883  dfon2lem3  35977  bj-peircestab  36753  bj-0int  37306  ptrecube  37821  fzmul  37942  zerdivemp1x  38148  psshepw  44029  ndmaovdistr  47453  ssfz12  47560  fzopredsuc  47569  smonoord  47617  elsetpreimafvbi  47637  iccpartltu  47671  iccpartgtl  47672  ichreuopeq  47719  elsprel  47721  lighneallem3  47853  odd2prm2  47964  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  bgoldbnnsum3prm  48050  clnbgrgrimlem  48179  grtrif1o  48188  grtriclwlk3  48191  gpgprismgr4cycllem7  48347  pgnbgreunbgr  48371  ringcbasbasALTV  48558  ply1mulgsumlem2  48633  ldepsnlinclem1  48751  ldepsnlinclem2  48752  nnolog2flm1  48836  blengt1fldiv2p1  48839