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  3716  ssprsseq  4779  preqsnd  4813  elpr2elpr  4823  disjxiun  5092  oprabidw  7384  oprabid  7385  elovmporab  7599  elovmporab1w  7600  elovmporab1  7601  mpoxopoveqd  8161  wfr3g  8259  oewordri  8517  fsuppunbi  9298  frr3g  9671  r1sdom  9689  updjud  9849  kmlem4  10067  kmlem12  10075  domtriomlem  10355  zorn2lem6  10414  axdclem  10432  wunr1om  10632  tskr1om  10680  zindd  12595  hash2pwpr  14401  fi1uzind  14432  swrdnd0  14582  pfxccatin12  14657  repsdf2  14702  2cshwcshw  14750  cshwcshid  14752  fprodmodd  15922  alzdvds  16249  pwp1fsum  16320  lcmfdvds  16571  prm23ge5  16745  cshwshashlem2  17026  0ringnnzr  20428  01eq0ringOLD  20434  ringcbasbas  20576  psgndiflemA  21526  mplcoe5lem  21962  gsummoncoe1  22211  gsummatr01lem3  22560  mp2pm2mplem4  22712  fiinopn  22804  cnmptcom  23581  fgcl  23781  fmfnfmlem1  23857  fmco  23864  flffbas  23898  cnpflf2  23903  metcnp3  24444  tngngp3  24560  clmvscom  25006  cphsscph  25167  aalioulem2  26257  elntg2  28948  ausgrusgrb  29128  usgredg4  29180  nbgr1vtx  29321  uhgr0edg0rgrb  29538  uhgrwkspth  29718  usgr2wlkspth  29722  uspgrn2crct  29771  crctcshwlkn0  29784  wwlksnredwwlkn  29858  wwlksnextsurj  29863  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  frgrnbnb  30255  frgrwopreglem5  30283  frgrwopreglem5ALT  30284  cvati  32328  dmdbr5ati  32384  loop1cycl  35112  sat1el2xp  35354  antnest  35664  dfon2lem3  35761  bj-peircestab  36529  bj-0int  37077  ptrecube  37602  fzmul  37723  zerdivemp1x  37929  psshepw  43764  ndmaovdistr  47195  ssfz12  47302  fzopredsuc  47311  smonoord  47359  elsetpreimafvbi  47379  iccpartltu  47413  iccpartgtl  47414  ichreuopeq  47461  elsprel  47463  lighneallem3  47595  odd2prm2  47706  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbnnsum3prm  47792  clnbgrgrimlem  47921  grtrif1o  47930  grtriclwlk3  47933  gpgprismgr4cycllem7  48089  pgnbgreunbgr  48113  ringcbasbasALTV  48300  ply1mulgsumlem2  48376  ldepsnlinclem1  48494  ldepsnlinclem2  48495  nnolog2flm1  48579  blengt1fldiv2p1  48582