NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  bitr3i GIF version

Theorem bitr3i 242
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 193 . 2 (φψ)
3 bitr3i.2 . 2 (ψχ)
42, 3bitri 240 1 (φχ)
Colors of variables: wff setvar class
Syntax hints:  wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  3bitrri  263  3bitr3i  266  3bitr3ri  267  xchnxbi  299  ianor  474  orordi  516  orordir  517  anandi  801  anandir  802  trunantru  1354  falnanfal  1357  cadan  1392  had0  1403  nic-axALT  1439  sbelx  2124  2mos  2283  2eu6  2289  abeq1i  2461  necon1bbii  2568  r19.41  2763  2ralor  2780  rexcom4a  2879  moeq  3012  euind  3023  2reuswap  3038  2reu5  3044  sbcid  3062  sbcco2  3069  sbc7  3073  sbcie2g  3079  eqsbc3  3085  sbcralt  3118  csbid  3143  cbvralcsf  3198  cbvrabcsf  3201  abss  3335  ssab  3336  difrab  3529  neq0  3560  vdif0  3610  ssunsn2  3865  sspr  3869  sstp  3870  prsspw  3878  disj5  3890  uniintsn  3963  dfpw12  4301  insklem  4304  nnsucelrlem3  4426  ltfinex  4464  dfevenfin2  4512  dfoddfin2  4513  proj1op  4600  proj2op  4601  unopab  4638  brab1  4684  opelssetsn  4760  eliunxp  4821  ralxp  4825  rexxp  4826  opelco  4884  cnvco  4894  dmun  4912  elimapw12  4945  iss  5000  imai  5010  imasn  5018  cotr  5026  cnvsym  5027  intasym  5028  intirr  5029  rninxp  5060  dffun2  5119  dffun3  5120  fin  5246  funimass4  5368  fnressn  5438  fvi  5442  resoprab  5581  ov6g  5600  fmpt2x  5730  braddcfn  5826  fnsex  5832  brpprod  5839  fnfullfunlem1  5856  fvfullfunlem2  5862  clos1induct  5880  transex  5910  connexex  5913  foundex  5914  qsexg  5982  enex  6031  xpassen  6057  enpw1pw  6075  enprmaplem1  6076  ovmuc  6130  ovcelem1  6171  ceex  6174  tcfnex  6244  nmembers1lem1  6268  frecxp  6314  fnfreclem2  6318  fnfreclem3  6319
  Copyright terms: Public domain W3C validator