MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr4ri Unicode version

Theorem 3bitr4ri 278
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)
Hypotheses
Ref Expression
3bitr4i.1
3bitr4i.2
3bitr4i.3
Assertion
Ref Expression
3bitr4ri

Proof of Theorem 3bitr4ri
StepHypRef Expression
1 3bitr4i.2 . 2
2 3bitr4i.1 . . 3
3 3bitr4i.3 . . 3
42, 3bitr4i 252 . 2
51, 4bitr2i 250 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  pm4.78  582  xor  891  nannan  1348  nanbiOLD  1353  nic-ax  1506  2sb5  2187  2sb6  2188  2sb5rf  2195  moabs  2315  2mo2  2372  2eu7  2385  2eu8  2386  r3al  2837  r2exlem  2977  risset  2982  r19.35  3004  ralxpxfr2d  3224  reuind  3303  undif3  3758  unab  3764  inab  3765  inssdif0  3895  ssundif  3911  snss  4154  raldifsnb  4161  pwtp  4246  unipr  4262  uni0b  4274  iinuni  4414  reusv2lem4  4656  pwtr  4705  elxp2  5022  opthprc  5052  xpiundir  5060  elvvv  5064  xpsspwOLD  5122  relun  5124  inopab  5138  difopab  5139  ralxpf  5154  dmiun  5216  rniun  5421  cnvresima  5501  imaco  5517  fnopabg  5709  dff1o2  5826  brprcneu  5864  fnsuppresOLD  6131  idref  6153  imaiun  6157  sorpss  6585  opabex3d  6778  opabex3  6779  ovmptss  6881  fnsuppres  6946  rankc1  8309  aceq1  8519  dfac10  8538  fin41  8845  axgroth6  9227  genpass  9408  infm3  10527  prime  10968  elixx3g  11571  elfz2  11708  elfzuzb  11711  rpnnen2  13959  divalgb  14062  1nprm  14222  maxprmfct  14254  vdwmc  14496  imasleval  14938  issubm  15978  issubg3  16219  efgrelexlemb  16768  ist1-2  19848  unisngl  20028  elflim2  20465  isfcls  20510  istlm  20687  isnlm  21184  ishl2  21810  0wlk  24547  0trl  24548  erclwwlkref  24813  erclwwlknref  24825  h1de2ctlem  26473  nonbooli  26569  5oalem7  26578  ho01i  26747  rnbra  27026  cvnbtwn3  27207  chrelat2i  27284  moel  27382  uniinn0  27424  disjex  27451  mptfnf  27499  maprnin  27554  ordtconlem1  27906  eulerpartgbij  28311  eulerpartlemr  28313  eulerpartlemn  28320  ballotlem2  28427  iscvm  28704  untuni  29081  dfso3  29097  dffr5  29182  nofulllem5  29466  brtxpsd3  29546  brbigcup  29548  fixcnv  29558  ellimits  29560  elfuns  29565  brimage  29576  brcart  29582  brimg  29587  brapply  29588  brcup  29589  brcap  29590  dfrdg4  29600  dfint3  29602  ellines  29802  mblfinlem2  30052  elicc3  30135  iscrngo2  30395  prtlem70  30592  prtlem100  30596  n0el  30600  prtlem15  30616  prter2  30622  inisegn0  30989  aaitgo  31111  isdomn3  31164  2sbc6g  31322  2sbc5g  31323  2reu7  32196  2reu8  32197  alsconv  33205  bnj976  33836  bnj1185  33852  bnj543  33951  bnj571  33964  bnj611  33976  bnj916  33991  bnj1000  33999  bnj1040  34028  bj-snsetex  34521  bj-snglc  34527  bj-projun  34552  lcvnbtwn3  34753  ishlat1  35077  ishlat2  35078  hlrelat2  35127  islpln5  35259  islvol5  35303  pclclN  35615  cdleme0nex  36015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator