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

Theorem bitr3i 185
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3i.1 (𝜓𝜑)
bitr3i.2 (𝜓𝜒)
Assertion
Ref Expression
bitr3i (𝜑𝜒)

Proof of Theorem bitr3i
StepHypRef Expression
1 bitr3i.1 . . 3 (𝜓𝜑)
21bicomi 131 . 2 (𝜑𝜓)
3 bitr3i.2 . 2 (𝜓𝜒)
42, 3bitri 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:  3bitrri  206  3bitr3i  209  3bitr3ri  210  anandi  564  anandir  565  xchnxbi  654  orordi  747  orordir  748  sbco3v  1920  elsb3  1929  elsb4  1930  sbco4  1960  abeq1i  2229  r19.41  2563  rexcom4a  2684  moeq  2832  mosubt  2834  2reuswapdc  2861  nfcdeq  2879  sbcid  2897  sbcco2  2904  sbc7  2908  sbcie2g  2914  eqsbc3  2920  sbcralt  2957  sbcrext  2958  cbvralcsf  3032  cbvrexcsf  3033  cbvrabcsf  3035  abss  3136  ssab  3137  difrab  3320  abn0m  3358  prsspw  3662  disjnim  3890  brab1  3945  unopab  3977  exss  4119  uniuni  4342  elvvv  4572  eliunxp  4648  ralxp  4652  rexxp  4653  opelco  4681  reldm0  4727  resieq  4799  resiexg  4834  iss  4835  imai  4865  cnvsym  4892  intasym  4893  asymref  4894  codir  4897  poirr2  4901  rninxp  4952  cnvsom  5052  funopg  5127  fin  5279  f1cnvcnv  5309  fndmin  5495  resoprab  5835  mpo2eqb  5848  ov6g  5876  offval  5957  dfopab2  6055  dfoprab3s  6056  fmpox  6066  spc2ed  6098  brtpos0  6117  dftpos3  6127  tpostpos  6129  ercnv  6418  xpcomco  6688  xpassen  6692  phpm  6727  ctssdccl  6964  elni2  7090  elfz2nn0  9860  elfzmlbp  9877  clim0  11022  isstructim  11900  ntreq0  12228  cnmptcom  12394  dedekindicclemicc  12706
  Copyright terms: Public domain W3C validator