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  3709  ssprsseq  4778  preqsnd  4812  elpr2elpr  4822  disjxiun  5092  oprabidw  7385  oprabid  7386  elovmporab  7600  elovmporab1w  7601  elovmporab1  7602  mpoxopoveqd  8159  wfr3g  8257  oewordri  8515  fsuppunbi  9282  frr3g  9658  r1sdom  9676  updjud  9836  kmlem4  10054  kmlem12  10062  domtriomlem  10342  zorn2lem6  10401  axdclem  10419  wunr1om  10619  tskr1om  10667  zindd  12582  hash2pwpr  14387  fi1uzind  14418  swrdnd0  14569  pfxccatin12  14644  repsdf2  14689  2cshwcshw  14736  cshwcshid  14738  fprodmodd  15908  alzdvds  16235  pwp1fsum  16306  lcmfdvds  16557  prm23ge5  16731  cshwshashlem2  17012  0ringnnzr  20444  01eq0ringOLD  20450  ringcbasbas  20592  psgndiflemA  21542  mplcoe5lem  21977  gsummoncoe1  22226  gsummatr01lem3  22575  mp2pm2mplem4  22727  fiinopn  22819  cnmptcom  23596  fgcl  23796  fmfnfmlem1  23872  fmco  23879  flffbas  23913  cnpflf2  23918  metcnp3  24458  tngngp3  24574  clmvscom  25020  cphsscph  25181  aalioulem2  26271  elntg2  28967  ausgrusgrb  29147  usgredg4  29199  nbgr1vtx  29340  uhgr0edg0rgrb  29557  uhgrwkspth  29737  usgr2wlkspth  29741  uspgrn2crct  29790  crctcshwlkn0  29803  wwlksnredwwlkn  29877  wwlksnextsurj  29882  hashecclwwlkn1  30061  umgrhashecclwwlk  30062  frgrnbnb  30277  frgrwopreglem5  30305  frgrwopreglem5ALT  30306  cvati  32350  dmdbr5ati  32406  loop1cycl  35204  sat1el2xp  35446  antnest  35756  dfon2lem3  35850  bj-peircestab  36620  bj-0int  37168  ptrecube  37683  fzmul  37804  zerdivemp1x  38010  psshepw  43908  ndmaovdistr  47334  ssfz12  47441  fzopredsuc  47450  smonoord  47498  elsetpreimafvbi  47518  iccpartltu  47552  iccpartgtl  47553  ichreuopeq  47600  elsprel  47602  lighneallem3  47734  odd2prm2  47845  nnsum4primeseven  47927  nnsum4primesevenALTV  47928  bgoldbnnsum3prm  47931  clnbgrgrimlem  48060  grtrif1o  48069  grtriclwlk3  48072  gpgprismgr4cycllem7  48228  pgnbgreunbgr  48252  ringcbasbasALTV  48439  ply1mulgsumlem2  48515  ldepsnlinclem1  48633  ldepsnlinclem2  48634  nnolog2flm1  48718  blengt1fldiv2p1  48721