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  585  anandir  586  xchnxbi  675  orordi  768  orordir  769  sbco3v  1962  sbco4  2000  elsb1  2148  elsb2  2149  abeq1i  2282  cbvabw  2293  r19.41  2625  rexcom4a  2754  moeq  2905  mosubt  2907  2reuswapdc  2934  nfcdeq  2952  sbcid  2970  sbcco2  2977  sbc7  2981  sbcie2g  2988  eqsbc1  2994  sbcralt  3031  sbcrext  3032  cbvralcsf  3111  cbvrexcsf  3112  cbvrabcsf  3114  abss  3216  ssab  3217  difrab  3401  abn0m  3440  prsspw  3752  disjnim  3980  brab1  4036  unopab  4068  exss  4212  uniuni  4436  elvvv  4674  eliunxp  4750  ralxp  4754  rexxp  4755  opelco  4783  reldm0  4829  resieq  4901  resiexg  4936  iss  4937  imai  4967  cnvsym  4994  intasym  4995  asymref  4996  codir  4999  poirr2  5003  rninxp  5054  cnvsom  5154  funopg  5232  fin  5384  f1cnvcnv  5414  fndmin  5603  resoprab  5949  mpo2eqb  5962  ov6g  5990  offval  6068  dfopab2  6168  dfoprab3s  6169  fmpox  6179  spc2ed  6212  brtpos0  6231  dftpos3  6241  tpostpos  6243  ercnv  6534  xpcomco  6804  xpassen  6808  phpm  6843  ctssdccl  7088  elni2  7276  elfz2nn0  10068  elfzmlbp  10088  clim0  11248  nnwosdc  11994  isstructim  12430  ntreq0  12926  cnmptcom  13092  dedekindicclemicc  13404
  Copyright terms: Public domain W3C validator