MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl11 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 syl11.2 . . 3 (𝜃𝜑)
2 syl11.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl 17 . 2 (𝜃 → (𝜓𝜒))
43com12 32 1 (𝜓 → (𝜃𝜒))
Colors of variables: wff setvar class
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  3731  ssprsseq  4742  elpr2elpr  4783  disjxiun  5049  oprabidw  7180  oprabid  7181  elovmporab  7385  elovmporab1w  7386  elovmporab1  7387  mpoxopoveqd  7883  wfr3g  7949  oewordri  8214  fsuppunbi  8851  r1sdom  9200  updjud  9360  pr2ne  9429  kmlem4  9577  kmlem12  9585  domtriomlem  9862  zorn2lem6  9921  axdclem  9939  wunr1om  10139  tskr1om  10187  zindd  12080  hash2pwpr  13839  fi1uzind  13860  swrdnd0  14019  pfxccatin12  14095  repsdf2  14140  2cshwcshw  14187  cshwcshid  14189  fprodmodd  15351  alzdvds  15670  pwp1fsum  15740  lcmfdvds  15984  prm23ge5  16150  cshwshashlem2  16430  0ringnnzr  20042  01eq0ring  20045  mplcoe5lem  20248  gsummoncoe1  20472  psgndiflemA  20745  gsummatr01lem3  21266  mp2pm2mplem4  21417  fiinopn  21509  cnmptcom  22286  fgcl  22486  fmfnfmlem1  22562  fmco  22569  flffbas  22603  cnpflf2  22608  metcnp3  23150  tngngp3  23265  clmvscom  23698  cphsscph  23858  aalioulem2  24932  elntg2  26782  ausgrusgrb  26961  usgredg4  27010  nbgr1vtx  27151  uhgr0edg0rgrb  27367  uhgrwkspth  27547  usgr2wlkspth  27551  uspgrn2crct  27597  crctcshwlkn0  27610  wwlksnredwwlkn  27684  wwlksnextsurj  27689  hashecclwwlkn1  27865  umgrhashecclwwlk  27866  frgrnbnb  28081  frgrwopreglem5  28109  frgrwopreglem5ALT  28110  cvati  30152  dmdbr5ati  30208  loop1cycl  32441  sat1el2xp  32683  dfon2lem3  33087  frr3g  33178  bj-peircestab  33945  bj-0int  34461  ptrecube  35002  fzmul  35124  zerdivemp1x  35330  psshepw  40406  ndmaovdistr  43689  ssfz12  43797  fzopredsuc  43806  smonoord  43814  elsetpreimafvbi  43834  iccpartltu  43868  iccpartgtl  43869  ichreuopeq  43916  elsprel  43918  lighneallem3  44051  odd2prm2  44162  nnsum4primeseven  44244  nnsum4primesevenALTV  44245  bgoldbnnsum3prm  44248  ringcbasbas  44584  ringcbasbasALTV  44608  ply1mulgsumlem2  44721  ldepsnlinclem1  44840  ldepsnlinclem2  44841  nnolog2flm1  44930  blengt1fldiv2p1  44933
  Copyright terms: Public domain W3C validator