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  3629  ssprsseq  4587  elpr2elpr  4632  disjxiun  4883  oprabid  6953  elovmpt2rab  7157  elovmpt2rab1  7158  mpt2xopoveqd  7629  wfr3g  7695  oewordri  7956  fsuppunbi  8584  r1sdom  8934  updjud  9093  pr2ne  9161  kmlem4  9310  kmlem12  9318  domtriomlem  9599  zorn2lem6  9658  axdclem  9676  wunr1om  9876  tskr1om  9924  zindd  11830  hash2pwpr  13572  fi1uzind  13593  swrdnd0  13752  swrdccatin2  13856  pfxccatin12  13861  swrdccatin12OLD  13862  repsdf2  13924  2cshwcshw  13976  cshwcshid  13978  fprodmodd  15130  alzdvds  15449  pwp1fsum  15521  lcmfdvds  15761  prm23ge5  15924  cshwshashlem2  16202  0ringnnzr  19666  01eq0ring  19669  mplcoe5lem  19864  gsummoncoe1  20070  psgndiflemA  20343  gsummatr01lem3  20869  mp2pm2mplem4  21021  fiinopn  21113  cnmptcom  21890  fgcl  22090  fmfnfmlem1  22166  fmco  22173  flffbas  22207  cnpflf2  22212  metcnp3  22753  tngngp3  22868  clmvscom  23297  aalioulem2  24525  elntg2  26334  ausgrusgrb  26514  usgredg4  26563  nbgr1vtx  26705  uhgr0edg0rgrb  26922  wlkresOLD  27021  uhgrwkspth  27107  usgr2wlkspth  27111  uspgrn2crct  27157  crctcshwlkn0  27170  wwlksnredwwlkn  27257  wwlksnredwwlknOLD  27258  wwlksnextsurj  27264  wwlksnextsurOLD  27269  hashecclwwlkn1  27475  umgrhashecclwwlk  27476  frgrnbnb  27701  frgrwopreglem5  27729  frgrwopreglem5ALT  27730  cvati  29797  dmdbr5ati  29853  dfon2lem3  32278  frr3g  32368  bj-0int  33628  ptrecube  34035  fzmul  34161  zerdivemp1x  34370  psshepw  39038  ndmaovdistr  42248  ssfz12  42356  fzopredsuc  42365  smonoord  42373  iccpartltu  42393  iccpartgtl  42394  elsprel  42414  lighneallem3  42545  odd2prm2  42652  nnsum4primeseven  42713  nnsum4primesevenALTV  42714  bgoldbnnsum3prm  42717  ringcbasbas  43049  ringcbasbasALTV  43073  ply1mulgsumlem2  43190  ldepsnlinclem1  43309  ldepsnlinclem2  43310  nnolog2flm1  43399  blengt1fldiv2p1  43402