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

Theorem bitr3i 184
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 130 . 2 (𝜑𝜓)
3 bitr3i.2 . 2 (𝜓𝜒)
42, 3bitri 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:  3bitrri  205  3bitr3i  208  3bitr3ri  209  anandi  557  anandir  558  xchnxbi  640  orordi  725  orordir  726  sbco3v  1891  elsb3  1900  elsb4  1901  sbco4  1931  abeq1i  2199  r19.41  2522  rexcom4a  2643  moeq  2790  mosubt  2792  2reuswapdc  2819  nfcdeq  2837  sbcid  2855  sbcco2  2862  sbc7  2866  sbcie2g  2872  eqsbc3  2878  sbcralt  2915  sbcrext  2916  cbvralcsf  2990  cbvrexcsf  2991  cbvrabcsf  2993  abss  3090  ssab  3091  difrab  3273  abn0m  3308  prsspw  3609  disjnim  3836  brab1  3890  unopab  3917  exss  4054  uniuni  4273  elvvv  4501  eliunxp  4575  ralxp  4579  rexxp  4580  opelco  4608  reldm0  4654  resieq  4723  resiexg  4757  iss  4758  imai  4788  cnvsym  4815  intasym  4816  asymref  4817  codir  4820  poirr2  4824  rninxp  4874  cnvsom  4974  funopg  5048  fin  5197  f1cnvcnv  5227  fndmin  5406  resoprab  5741  mpt22eqb  5754  ov6g  5782  offval  5863  dfopab2  5959  dfoprab3s  5960  fmpt2x  5970  spc2ed  5998  brtpos0  6017  dftpos3  6027  tpostpos  6029  ercnv  6311  xpcomco  6540  xpassen  6544  phpm  6579  elni2  6871  elfz2nn0  9522  elfzmlbp  9539  clim0  10669  isstructim  11504
  Copyright terms: Public domain W3C validator