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

Theorem 3bitr4i 210
 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 185 . 2 (𝜑𝜃)
51, 4bitri 182 1 (𝜒𝜃)
 Colors of variables: wff set class Syntax hints:   ↔ wb 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  bibi2d  230  pm4.71  381  pm5.32ri  443  mpan10  458  an31  529  an4  551  or4  721  ordir  764  andir  766  dcbii  781  3anrot  925  3orrot  926  3ancoma  927  3orcomb  929  3ioran  935  3anbi123i  1128  3orbi123i  1129  3or6  1255  xorcom  1320  nfbii  1403  19.26-3an  1413  alnex  1429  19.42h  1618  19.42  1619  equsal  1656  sb6  1808  eeeanv  1850  sbbi  1875  sbco3xzyz  1889  sbcom2v  1903  sbel2x  1916  sb8eu  1955  sb8mo  1956  sb8euh  1965  eu1  1967  cbvmo  1982  mo3h  1995  sbmo  2001  eqcom  2084  abeq1  2189  cbvab  2202  clelab  2204  nfceqi  2216  sbabel  2245  ralbii2  2377  rexbii2  2378  r2alf  2384  r2exf  2385  nfraldya  2401  nfrexdya  2402  r3al  2409  r19.41  2510  r19.42v  2512  ralcomf  2516  rexcomf  2517  reean  2523  3reeanv  2525  rabid2  2531  rabbi  2532  reubiia  2539  rmobiia  2544  reu5  2567  rmo5  2570  cbvralf  2572  cbvrexf  2573  cbvreu  2576  cbvrmo  2577  vjust  2603  ceqsex3v  2642  ceqsex4v  2643  ceqsex8v  2645  eueq  2764  reu2  2781  reu6  2782  reu3  2783  rmo4  2786  2rmorex  2797  cbvsbc  2843  sbccomlem  2889  rmo3  2906  csbabg  2964  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  eqss  3015  uniiunlem  3083  ssequn1  3143  unss  3147  rexun  3153  ralunb  3154  elin3  3158  incom  3159  inass  3177  ssin  3189  ssddif  3199  unssdif  3200  difin  3202  invdif  3207  indif  3208  indi  3212  symdifxor  3231  disj3  3297  rexsns  3434  reusn  3465  prss  3543  tpss  3552  eluni2  3607  elunirab  3616  uniun  3622  uni0b  3628  unissb  3633  elintrab  3650  ssintrab  3661  intun  3669  intpr  3670  iuncom  3686  iuncom4  3687  iunab  3726  ssiinf  3729  iinab  3741  iunin2  3743  iunun  3757  iunxun  3758  iunxiun  3759  sspwuni  3762  iinpw  3765  cbvdisj  3778  brun  3833  brin  3834  brdif  3835  dftr2  3879  inuni  3932  repizf2lem  3937  unidif0  3943  ssext  3978  pweqb  3980  otth2  3998  opelopabsbALT  4016  eqopab2b  4036  pwin  4039  unisuc  4170  sucexb  4243  elnn  4348  xpiundi  4418  xpiundir  4419  poinxp  4429  soinxp  4430  seinxp  4431  inopab  4490  difopab  4491  raliunxp  4499  rexiunxp  4500  iunxpf  4506  cnvco  4542  dmiun  4566  dmuni  4567  dm0rn0  4574  brres  4640  dmres  4654  cnvsym  4732  asymref  4734  codir  4737  qfto  4738  cnvopab  4750  cnvdif  4754  rniun  4758  dminss  4762  imainss  4763  cnvcnvsn  4821  resco  4849  imaco  4850  rnco  4851  coiun  4854  coass  4863  ressn  4882  cnviinm  4883  xpcom  4888  funcnv  4985  funcnv3  4986  fncnv  4990  fun11  4991  fnres  5040  dfmpt3  5046  fnopabg  5047  fintm  5100  fin  5101  fores  5140  dff1o3  5157  fun11iun  5172  f11o  5184  f1ompt  5346  fsn  5361  imaiun  5425  isores2  5478  eqoprab2b  5588  opabex3d  5773  opabex3  5774  dfopab2  5840  dfoprab3s  5841  fmpt2x  5851  tpostpos  5907  dfsmo2  5930  qsid  6230  xpassen  6364  diffitest  6411  supmoti  6455  eqinfti  6482  distrnqg  6628  ltbtwnnq  6657  distrnq0  6700  nqprrnd  6784  ltresr  7058  elznn0nn  8435  xrnemnf  8918  xrnepnf  8919  elioomnf  9056  elxrge0  9066  elfzuzb  9104  fzass4  9145  elfz2nn0  9194  elfzo2  9226  elfzo3  9238  lbfzo0  9256  fzind2  9314  rexfiuz  10002  infssuzex  10478  bdceq  10776
 Copyright terms: Public domain W3C validator