NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  com12 Unicode version

Theorem com12 27
Description: Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1
Assertion
Ref Expression
com12

Proof of Theorem com12
StepHypRef Expression
1 id 19 . 2
2 com12.1 . 2
31, 2syl5com 26 1
Colors of variables: wff setvar class
Syntax hints:   wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
This theorem is referenced by:  syl5  28  syl6com  31  mpcom  32  syli  33  pm2.27  35  pm2.43b  46  syl9r  67  com3r  73  pm2.86i  92  pm2.24  101  con3rr3  128  expt  148  jad  154  pm2.61  163  syl5ibcom  211  syl5ibrcom  213  pm5.501  330  jaod  369  orel1  371  pm2.62  398  impcom  419  imp3a  420  expcom  424  exp3a  425  pm3.21  435  imdistanri  672  pm2.64  764  pm2.75  822  ccased  913  dedlem0b  919  3impd  1165  3expd  1168  mp3an1i  1270  simplbi2com  1374  meredith  1404  sbequ2  1650  equtrr  1683  ax12olem1  1927  ax12olem3  1929  ax10lem4  1941  ax11b  1995  sb6rf  2091  sb56  2098  exsb  2130  mo  2226  exmoeu  2246  morimv  2252  eupickbi  2270  2mo  2282  2eu1  2284  exists2  2294  r19.12  2727  2gencl  2888  3gencl  2889  rspccv  2952  ceqex  2969  mob  3018  euind  3023  reuind  3039  2rmorex  3040  sseq2  3293  reupick2  3541  uneqdifeq  3638  difsn  3845  eqsn  3867  iinss2  4018  sspwb  4118  pwadjoin  4119  preq12b  4127  iotaval  4350  nncaddccl  4419  nnsucelrlem2  4425  nndisjeq  4429  ltfintri  4466  ncfinraise  4481  ncfinlower  4483  tfin11  4493  tfinltfinlem1  4500  sucoddeven  4511  evenoddnnnul  4514  evenodddisj  4516  eventfin  4517  oddtfin  4518  sfindbl  4530  spfinsfincl  4539  vfinspsslem1  4550  vfinspss  4551  vfinspeqtncv  4553  phi11lem1  4595  copsexg  4607  2optocl  4839  3optocl  4840  xp11  5056  funmo  5125  fss  5230  fv3  5341  tz6.12c  5347  tz6.12i  5348  funfvima  5459  fvclss  5462  f1fveq  5473  isotr  5495  oprabid  5550  clos1conn  5879  2ecoptocl  5997  3ecoptocl  5998  enprmaplem3  6078  enprmaplem5  6080  nenpw1pwlem2  6085  leconnnc  6218  letc  6231  ce2le  6233  nclenn  6249  nchoicelem17  6305  nchoicelem19  6307  fnfreclem3  6319  fnfrec  6320
  Copyright terms: Public domain W3C validator