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

Theorem 3bitr4ri 307
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 281 . 2 (𝜑𝜃)
51, 4bitr2i 279 1 (𝜃𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 209
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 210
This theorem is referenced by:  biadan  818  pm4.78  932  xor  1012  cases2  1043  noranOLD  1528  nic-ax  1675  2sb6  2095  2sb5  2284  dfsb7  2287  2sb5rf  2498  2sb6rf  2499  eu6lem  2659  eu6  2660  2mo2  2735  2eu7  2746  2eu8  2747  euae  2748  ralanidOLD  3164  r3al  3197  risset  3259  r2exlem  3294  ralxpxfr2d  3625  reuind  3730  undif3  4250  unab  4255  inab  4256  n0el  4304  inssdif0  4312  ssundif  4416  ralf0  4440  raldifsnb  4713  pwtp  4819  unipr  4841  uni0b  4850  iinuni  5006  reusv2lem4  5289  pwtr  5332  opthprc  5603  xpiundir  5610  xpsspw  5669  relun  5671  inopab  5688  difopab  5689  ralxpf  5704  dmiun  5769  elidinxp  5898  iresn0n0  5910  inisegn0  5948  rniun  5993  imaco  6091  rnco  6092  mptfnf  6472  fnopabg  6474  dff1o2  6611  brprcneu  6653  idref  6899  imaiun  6996  sorpss  7448  opabex3d  7661  opabex3rd  7662  opabex3  7663  ovmptss  7784  fnsuppres  7853  rankc1  9296  aceq1  9541  dfac10  9561  fin41  9864  axgroth6  10248  genpass  10429  infm3  11596  prime  12060  elixx3g  12748  elfz2  12901  elfzuzb  12905  rpnnen2lem12  15578  divalgb  15753  1nprm  16021  maxprmfct  16051  vdwmc  16312  imasleval  16814  issubm  17968  issubg3  18297  efgrelexlemb  18876  ist1-2  21955  unisngl  22135  elflim2  22572  isfcls  22617  istlm  22793  isnlm  23284  ishl2  23977  ovoliunlem1  24109  erclwwlkref  27808  erclwwlknref  27857  0wlk  27904  h1de2ctlem  29341  nonbooli  29437  5oalem7  29446  ho01i  29614  rnbra  29893  cvnbtwn3  30074  chrelat2i  30151  nelbOLD  30241  moel  30261  difrab2  30270  uniinn0  30313  disjex  30353  maprnin  30478  ordtconnlem1  31224  esum2dlem  31408  eulerpartgbij  31687  eulerpartlemr  31689  eulerpartlemn  31696  ballotlem2  31803  bnj976  32106  bnj1185  32122  bnj543  32222  bnj571  32235  bnj611  32247  bnj916  32262  bnj1000  32270  bnj1040  32301  iscvm  32563  untuni  32992  dfso3  33007  dffr5  33046  elima4  33076  brtxpsd3  33414  brbigcup  33416  fixcnv  33426  ellimits  33428  elfuns  33433  brimage  33444  brcart  33450  brimg  33455  brapply  33456  brcup  33457  brcap  33458  dfrdg4  33469  dfint3  33470  ellines  33670  elicc3  33722  bj-snsetex  34343  bj-snglc  34349  bj-projun  34374  bj-vjust  34414  wl-2xor  34842  wl-cases2-dnf  34862  poimirlem27  35029  mblfinlem2  35040  iscrngo2  35380  n0elqs  35688  inxpxrn  35748  eqvrelcoss3  35958  prtlem70  36098  prtlem100  36100  prtlem15  36116  prter2  36122  lcvnbtwn3  36269  ishlat1  36593  ishlat2  36594  hlrelat2  36644  islpln5  36776  islvol5  36820  pclclN  37132  cdleme0nex  37531  aaitgo  40022  isdomn3  40064  imaiun1  40268  relexp0eq  40318  ntrk1k3eqk13  40672  2sbc6g  41039  2sbc5g  41040  2reu7  43593  2reu8  43594  alsconv  45244
  Copyright terms: Public domain W3C validator