Theorem syl11 34

Description: A syllogism inference. Commuted form of an instance of syl 18. (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 18	. 2 ⊢ (𝜃 → (𝜓 → 𝜒))
4	3	com12 33	1 ⊢ (𝜓 → (𝜃 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imbibi  396  2rmorex  3711  ssprsseq  4785  preqsnd  4818  elpr2elpr  4828  disjxiun  5099  oprabidw  7451  oprabid  7452  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  mpoxopoveqd  8238  wfr3g  8337  oewordri  8601  fsuppunbi  9381  frr3g  9760  r1sdom  9781  updjud  10015  kmlem4  10232  kmlem12  10240  domtriomlem  10520  zorn2lem6  10579  axdclem  10597  wunr1om  10804  tskr1om  10852  zindd  12800  hash2pwpr  14621  fi1uzind  14652  swrdnd0  14807  pfxccatin12  14882  repsdf2  14929  2cshwcshw  14976  cshwcshid  14978  fprodmodd  16164  alzdvds  16490  pwp1fsum  16561  lcmfdvds  16817  prm23ge5  16993  cshwshashlem2  17274  0ringnnzr  20776  01eq0ringOLD  20782  ringcbasbas  20925  isfieldidl  21540  psgndiflemA  21907  mplcoe5lem  22348  gsummoncoe1  22626  gsummatr01lem3  22972  mp2pm2mplem4  23127  fiinopn  23219  cnmptcom  23997  fgcl  24197  fmfnfmlem1  24273  fmco  24280  flffbas  24314  cnpflf2  24319  metcnp3  24859  tngngp3  24975  clmvscom  25411  cphsscph  25572  aalioulem2  26660  elntg2  29563  ausgrusgrb  29746  usgredg4  29798  nbgr1vtx  29939  uhgr0edg0rgrb  30155  uhgrwkspth  30341  usgr2wlkspth  30345  uspgrn2crct  30397  crctcshwlkn0  30410  wwlksnredwwlkn  30484  wwlksnextsurj  30489  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  loop1cycl  30744  frgrnbnb  30894  frgrwopreglem5  30922  frgrwopreglem5ALT  30923  cvati  32968  dmdbr5ati  33024  sat1el2xp  36186  antnest  36496  dfon2lem3  36589  bj-peircestab  37462  bj-0int  38064  ptrecube  38581  fzmul  38718  zerdivemp1x  38924  psshepw  44830  ndmaovdistr  48319  ssfz12  48426  fzopredsuc  48436  smonoord  48489  elsetpreimafvbi  48515  iccpartltu  48549  iccpartgtl  48550  ichreuopeq  48597  elsprel  48599  lighneallem3  48734  odd2prm2  48858  nnsum4primeseven  48940  nnsum4primesevenALTV  48941  bgoldbnnsum3prm  48944  clnbgrgrimlem  49073  grtrif1o  49082  grtriclwlk3  49085  gpgprismgr4cycllem7  49241  pgnbgreunbgr  49265  ringcbasbasALTV  49451  ply1mulgsumlem2  49541  ldepsnlinclem1  49659  ldepsnlinclem2  49660  nnolog2flm1  49744  blengt1fldiv2p1  49747