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

Theorem 3bitr4ri 305
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 279 . 2 (𝜑𝜃)
51, 4bitr2i 277 1 (𝜃𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  biadan  815  pm4.78  928  xor  1008  cases2  1039  noranOLD  1518  nic-ax  1665  2sb6  2085  2sb5  2273  dfsb7  2276  2sb5rf  2488  2sb6rf  2489  eu6lem  2651  eu6  2652  2mo2  2725  2eu7  2738  2eu8  2739  euae  2740  ralanidOLD  3166  r3al  3199  risset  3264  r2exlem  3299  ralxpxfr2d  3636  reuind  3741  undif3  4262  unab  4267  inab  4268  n0el  4318  inssdif0  4326  ssundif  4429  ralf0  4453  raldifsnb  4721  pwtp  4825  unipr  4843  uni0b  4855  iinuni  5011  reusv2lem4  5292  pwtr  5336  opthprc  5609  xpiundir  5616  xpsspw  5675  relun  5677  inopab  5694  difopab  5695  ralxpf  5710  dmiun  5775  elidinxp  5904  iresn0n0  5916  inisegn0  5954  rniun  5999  imaco  6097  rnco  6098  mptfnf  6476  fnopabg  6478  dff1o2  6613  brprcneu  6655  idref  6900  imaiun  6995  sorpss  7443  opabex3d  7655  opabex3rd  7656  opabex3  7657  ovmptss  7777  fnsuppres  7846  rankc1  9287  aceq1  9531  dfac10  9551  fin41  9854  axgroth6  10238  genpass  10419  infm3  11588  prime  12051  elixx3g  12739  elfz2  12887  elfzuzb  12890  rpnnen2lem12  15566  divalgb  15743  1nprm  16011  maxprmfct  16041  vdwmc  16302  imasleval  16802  issubm  17956  issubg3  18235  efgrelexlemb  18805  ist1-2  21883  unisngl  22063  elflim2  22500  isfcls  22545  istlm  22720  isnlm  23211  ishl2  23900  ovoliunlem1  24030  erclwwlkref  27725  erclwwlknref  27775  0wlk  27822  h1de2ctlem  29259  nonbooli  29355  5oalem7  29364  ho01i  29532  rnbra  29811  cvnbtwn3  29992  chrelat2i  30069  nelbOLD  30159  moel  30179  difrab2  30188  uniinn0  30229  disjex  30270  maprnin  30393  ordtconnlem1  31066  esum2dlem  31250  eulerpartgbij  31529  eulerpartlemr  31531  eulerpartlemn  31538  ballotlem2  31645  bnj976  31948  bnj1185  31964  bnj543  32064  bnj571  32077  bnj611  32089  bnj916  32104  bnj1000  32112  bnj1040  32141  iscvm  32403  untuni  32832  dfso3  32847  dffr5  32886  elima4  32916  brtxpsd3  33254  brbigcup  33256  fixcnv  33266  ellimits  33268  elfuns  33273  brimage  33284  brcart  33290  brimg  33295  brapply  33296  brcup  33297  brcap  33298  dfrdg4  33309  dfint3  33310  ellines  33510  elicc3  33562  bj-snsetex  34172  bj-snglc  34178  bj-projun  34203  bj-vjust  34240  wl-cases2-dnf  34634  poimirlem27  34800  mblfinlem2  34811  iscrngo2  35156  n0elqs  35464  inxpxrn  35523  eqvrelcoss3  35733  prtlem70  35873  prtlem100  35875  prtlem15  35891  prter2  35897  lcvnbtwn3  36044  ishlat1  36368  ishlat2  36369  hlrelat2  36419  islpln5  36551  islvol5  36595  pclclN  36907  cdleme0nex  37306  aaitgo  39640  isdomn3  39682  imaiun1  39874  relexp0eq  39924  ntrk1k3eqk13  40278  2sbc6g  40624  2sbc5g  40625  2reu7  43187  2reu8  43188  alsconv  44819
  Copyright terms: Public domain W3C validator