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 ⊢ (𝜓 → (𝜃 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imbibi  395  2rmorex  3718  ssprsseq  4792  preqsnd  4825  elpr2elpr  4835  disjxiun  5107  oprabidw  7443  oprabid  7444  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  mpoxopoveqd  8218  wfr3g  8317  oewordri  8579  fsuppunbi  9350  frr3g  9729  r1sdom  9747  updjud  9921  kmlem4  10138  kmlem12  10146  domtriomlem  10427  zorn2lem6  10486  axdclem  10504  wunr1om  10705  tskr1om  10753  zindd  12698  hash2pwpr  14515  fi1uzind  14546  swrdnd0  14697  pfxccatin12  14772  repsdf2  14817  2cshwcshw  14864  cshwcshid  14866  fprodmodd  16053  alzdvds  16379  pwp1fsum  16450  lcmfdvds  16701  prm23ge5  16876  cshwshashlem2  17157  0ringnnzr  20610  01eq0ringOLD  20616  ringcbasbas  20759  isfieldidl  21367  psgndiflemA  21732  mplcoe5lem  22171  gsummoncoe1  22449  gsummatr01lem3  22795  mp2pm2mplem4  22947  fiinopn  23039  cnmptcom  23816  fgcl  24016  fmfnfmlem1  24092  fmco  24099  flffbas  24133  cnpflf2  24138  metcnp3  24678  tngngp3  24794  clmvscom  25230  cphsscph  25391  aalioulem2  26477  elntg2  29316  ausgrusgrb  29496  usgredg4  29548  nbgr1vtx  29689  uhgr0edg0rgrb  29905  uhgrwkspth  30085  usgr2wlkspth  30089  uspgrn2crct  30138  crctcshwlkn0  30151  wwlksnredwwlkn  30225  wwlksnextsurj  30230  hashecclwwlkn1  30409  umgrhashecclwwlk  30410  frgrnbnb  30625  frgrwopreglem5  30653  frgrwopreglem5ALT  30654  cvati  32699  dmdbr5ati  32755  loop1cycl  35610  sat1el2xp  35852  antnest  36162  dfon2lem3  36256  bj-peircestab  37124  bj-0int  37724  ptrecube  38252  fzmul  38373  zerdivemp1x  38579  psshepw  44497  ndmaovdistr  47927  ssfz12  48034  fzopredsuc  48044  smonoord  48097  elsetpreimafvbi  48123  iccpartltu  48157  iccpartgtl  48158  ichreuopeq  48205  elsprel  48207  lighneallem3  48342  odd2prm2  48466  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  bgoldbnnsum3prm  48552  clnbgrgrimlem  48681  grtrif1o  48690  grtriclwlk3  48693  gpgprismgr4cycllem7  48849  pgnbgreunbgr  48873  ringcbasbasALTV  49060  ply1mulgsumlem2  49150  ldepsnlinclem1  49268  ldepsnlinclem2  49269  nnolog2flm1  49353  blengt1fldiv2p1  49356