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

Theorem bitr4i 243
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr4i.1 (φψ)
bitr4i.2 (χψ)
Assertion
Ref Expression
bitr4i (φχ)

Proof of Theorem bitr4i
StepHypRef Expression
1 bitr4i.1 . 2 (φψ)
2 bitr4i.2 . . 3 (χψ)
32bicomi 193 . 2 (ψχ)
41, 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:  3bitr2i  264  3bitr2ri  265  3bitr4i  268  3bitr4ri  269  imor  401  dfbi2  609  pm5.32  617  imdistan  670  imimorb  847  nbi2  862  pm5.6  878  mpbiran  884  mpbiran2  885  biluk  899  3anrev  945  nannan  1291  xorneg  1313  nic-ax  1438  nic-axALT  1439  19.43  1605  19.3v  1665  19.9vOLD  1697  equsalhwOLD  1839  nf3  1867  nf4  1868  equsal  1960  sb6x  2029  sb5f  2040  sb3an  2070  sbequ8  2079  sb5  2100  sbhb  2107  sbel2x  2125  eu2  2229  eu3  2230  eu5  2242  moanim  2260  2eu4  2287  2eu6  2289  cleqh  2450  cleqf  2513  necon3bii  2548  neor  2600  neorian  2603  r2alf  2649  r2exf  2650  r19.23t  2728  r19.26-3  2748  r19.26m  2749  r19.43  2766  rabid2  2788  isset  2863  ralv  2872  rexv  2873  reuv  2874  rmov  2875  rexcom4b  2880  ceqsex4v  2898  ceqsex8v  2900  ceqsrexv  2972  ralrab2  3002  rexrab2  3004  reu2  3024  reu3  3026  reueq  3033  2reuswap  3038  reuind  3039  2reu5lem3  3043  rmo2  3131  elun  3220  dblcompl  3227  dfss2  3262  dfss3  3263  dfss3f  3265  ssabral  3337  rabss  3343  uniiunlem  3353  sspsstri  3371  npss  3379  uncom  3408  inass  3465  nsspssun  3488  dfss4  3489  dfun2  3490  dfin2  3491  indi  3501  indifdir  3511  difin2  3516  complab  3524  reupick3  3540  necompl  3544  n0f  3558  eqv  3565  vss  3587  disj3  3595  undisj1  3602  undisj2  3603  inundif  3628  undif  3630  sscon34  3661  euabsn2  3791  euabsn  3792  pwpw0  3855  prssg  3862  ssunsn  3866  pwpr  3883  dfuni2  3893  unissb  3921  elint2  3933  ssint  3942  uniintab  3964  dfiin2g  4000  iunn0  4026  iunxun  4047  iunxiun  4048  iinpw  4054  sspwb  4118  elpw1  4144  elpw12  4145  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  eqpw1  4162  pw111  4170  eluni1g  4172  elvvk  4207  ssrelk  4211  eqrelk  4212  opkelimagekg  4271  imacok  4282  xpkvexg  4285  sikexlem  4295  dfimak2  4298  dfpw12  4301  insklem  4304  ndisjrelk  4323  dfpw2  4327  dfeu2  4333  dfiota2  4340  dfiota4  4372  dfaddc2  4381  dfnnc2  4395  nnc0suc  4412  elsuc  4413  addcass  4415  nnsucelrlem1  4424  nndisjeq  4429  preaddccan2lem1  4454  ltfinex  4464  ltfintrilem1  4465  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  nnpw1ex  4484  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnadjoinpw  4521  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  spfininduct  4540  vfinspsslem1  4550  vfinspss  4551  vfinncsp  4554  dfphi2  4569  dfop2lem1  4573  dfop2  4575  opeq  4619  br1stg  4730  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem6  4736  setconslem7  4737  df1st2  4738  dfswap2  4741  dfima2  4745  dfco1  4748  dfsi2  4751  brssetsn  4759  dfid3  4768  opelxp  4811  xpiundir  4818  raliunxp  4823  elxp3  4831  ssopr  4846  inxp  4863  cnvuni  4895  dmuni  4914  dm0rn0  4921  elimapw1  4944  elimapw12  4945  elimapw13  4946  elimapw11c  4948  ssdmres  4987  elres  4995  imadmrn  5008  cotr  5026  intirr  5029  cnvdif  5034  rnuni  5038  xpnz  5045  xp11  5056  dfco2  5080  resco  5085  rnco  5087  coiun  5090  coass  5097  dffun2  5119  dffun6f  5123  dffun7  5133  funfn  5136  fununi  5160  dffn2  5224  dffn3  5229  fint  5245  f1funfun  5263  dffn4  5275  dff1o2  5291  dff1o4  5294  eqfnfv3  5394  fsn  5432  abrexco  5463  imaiun  5464  dff13  5471  1stfo  5505  2ndfo  5506  cnvsi  5518  funsi  5520  oprabid  5550  eloprabga  5578  dmmpt  5683  dffn5v  5706  fnov2  5707  fnmpt2  5732  brimage  5793  fntxp  5804  otsnelsi3  5805  addcfnex  5824  funsex  5828  pw1fnf1o  5855  brfullfunop  5867  clos1induct  5880  dfnnc3  5885  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  frds  5935  ssetpov  5944  eqerlem  5960  qsexg  5982  entr  6038  fundmen  6043  unen  6048  xpen  6055  enmap1lem1  6069  enpw1pw  6075  enprmaplem1  6076  lecex  6115  elncs  6119  muccl  6132  mucex  6133  muccom  6134  mucass  6135  ncdisjeq  6148  ncssfin  6151  ovcelem1  6171  ceex  6174  ce0addcnnul  6179  cenc  6181  el2c  6191  sbthlem1  6203  sbthlem3  6205  leconnnc  6218  dflec3  6221  nclenc  6222  lenc  6223  tc11  6228  taddc  6229  letc  6231  ce2le  6233  tcfnex  6244  ncfin  6247  muc0or  6252  csucex  6259  addccan2nclem1  6263  nmembers1lem1  6268  nmembers1lem3  6270  nchoicelem3  6291  nchoicelem11  6299  nchoicelem16  6304  dmfrec  6316  fnfreclem3  6319
  Copyright terms: Public domain W3C validator