Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr4i GIF version

Theorem 3bitr4i 211
 Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitr4i.1 (𝜑𝜓)
3bitr4i.2 (𝜒𝜑)
3bitr4i.3 (𝜃𝜓)
Assertion
Ref Expression
3bitr4i (𝜒𝜃)

Proof of Theorem 3bitr4i
StepHypRef Expression
1 3bitr4i.2 . 2 (𝜒𝜑)
2 3bitr4i.1 . . 3 (𝜑𝜓)
3 3bitr4i.3 . . 3 (𝜃𝜓)
42, 3bitr4i 186 . 2 (𝜑𝜃)
51, 4bitri 183 1 (𝜒𝜃)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  bibi2d  231  pm4.71  387  pm5.32ri  451  mpan10  466  an31  554  an4  576  or4  761  ordir  807  andir  809  3anrot  968  3orrot  969  3ancoma  970  3orcomb  972  3ioran  978  3anbi123i  1171  3orbi123i  1172  3or6  1302  xorcom  1367  nfbii  1450  19.26-3an  1460  alnex  1476  19.42h  1663  19.42  1664  equsal  1701  sb6  1854  eeeanv  1901  sbbi  1927  sbco3xzyz  1941  sbcom2v  1953  sbel2x  1966  sb8eu  2003  sb8mo  2004  sb8euh  2013  eu1  2015  cbvmo  2030  mo3h  2043  sbmo  2049  eqcom  2143  abeq1  2251  cbvabw  2264  cbvab  2265  clelab  2267  nfceqi  2279  sbabel  2309  ralbii2  2450  rexbii2  2451  r2alf  2457  r2exf  2458  nfraldya  2474  nfrexdya  2475  r3al  2482  r19.41  2591  r19.42v  2593  ralcomf  2597  rexcomf  2598  reean  2604  3reeanv  2606  rabid2  2612  rabbi  2613  reubiia  2620  rmobiia  2625  reu5  2648  rmo5  2651  cbvralf  2653  cbvrexf  2654  cbvreu  2657  cbvrmo  2658  vjust  2692  ceqsex3v  2733  ceqsex4v  2734  ceqsex8v  2736  eueq  2861  reu2  2878  reu6  2879  reu3  2880  rmo4  2883  rmo3f  2887  2rmorex  2896  cbvsbcw  2942  cbvsbc  2943  sbccomlem  2989  rmo3  3006  csbabg  3068  cbvralcsf  3069  cbvrexcsf  3070  cbvreucsf  3071  eqss  3119  uniiunlem  3192  ssequn1  3253  unss  3257  rexun  3263  ralunb  3264  elin3  3274  incom  3275  inass  3293  ssin  3305  ssddif  3317  unssdif  3318  difin  3320  invdif  3325  indif  3326  indi  3330  symdifxor  3349  disj3  3422  eldifpr  3561  rexsns  3572  reusn  3604  prss  3686  tpss  3695  eluni2  3750  elunirab  3759  uniun  3765  uni0b  3771  unissb  3776  elintrab  3793  ssintrab  3804  intun  3812  intpr  3813  iuncom  3829  iuncom4  3830  iunab  3869  ssiinf  3872  iinab  3884  iunin2  3886  iunun  3901  iunxun  3902  iunxiun  3904  sspwuni  3907  iinpw  3913  cbvdisj  3926  brun  3989  brin  3990  brdif  3991  dftr2  4038  inuni  4090  repizf2lem  4095  unidif0  4101  ssext  4154  pweqb  4156  otth2  4174  opelopabsbALT  4192  eqopab2b  4212  pwin  4215  unisuc  4346  elpwpwel  4407  sucexb  4424  elomssom  4530  xpiundi  4609  xpiundir  4610  poinxp  4620  soinxp  4621  seinxp  4622  inopab  4683  difopab  4684  raliunxp  4692  rexiunxp  4693  iunxpf  4699  cnvco  4736  dmiun  4760  dmuni  4761  dm0rn0  4768  brres  4837  dmres  4852  cnvsym  4934  asymref  4936  codir  4939  qfto  4940  cnvopab  4952  cnvdif  4957  rniun  4961  dminss  4965  imainss  4966  cnvcnvsn  5027  resco  5055  imaco  5056  rnco  5057  coiun  5060  coass  5069  ressn  5091  cnviinm  5092  xpcom  5097  funcnv  5196  funcnv3  5197  fncnv  5201  fun11  5202  fnres  5251  dfmpt3  5257  fnopabg  5258  fintm  5320  fin  5321  fores  5366  dff1o3  5385  fun11iun  5400  f11o  5412  f1ompt  5583  fsn  5604  imaiun  5673  isores2  5726  eqoprab2b  5841  opabex3d  6031  opabex3  6032  dfopab2  6099  dfoprab3s  6100  fmpox  6110  tpostpos  6173  dfsmo2  6196  qsid  6506  mapval2  6584  mapsncnv  6601  elixp2  6608  ixpin  6629  xpassen  6736  diffitest  6793  pw1dc0el  6817  supmoti  6897  eqinfti  6924  distrnqg  7248  ltbtwnnq  7277  distrnq0  7320  nqprrnd  7404  ltresr  7700  elznn0nn  9121  xrnemnf  9623  xrnepnf  9624  elioomnf  9810  elxrge0  9820  elfzuzb  9860  fzass4  9902  elfz2nn0  9952  elfzo2  9987  elfzo3  10000  lbfzo0  10018  fzind2  10076  rexfiuz  10822  fisumcom2  11268  prodmodc  11408  infssuzex  11714  isbasis2g  12287  tgval2  12295  ntreq0  12376  txuni2  12500  isms2  12698  bdceq  13256
 Copyright terms: Public domain W3C validator