Theorem bitrid 282

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
bitrid.1	⊢ (𝜑 ↔ 𝜓)
bitrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitrid	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem bitrid

Step	Hyp	Ref	Expression
1		bitrid.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3		bitrid.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 278	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitr2id  284  bitr3id  285  3bitr4g  314  imim21b  395  ifpfal  1074  norass  1535  cad0OLD  1621  ax12wdemo  2131  eu6lem  2573  abbi  2810  necon3abid  2980  necon3bid  2988  ceqsralv  3469  ralxpxfr2d  3576  ceqsrexv  3585  ceqsrex2v  3587  elabg  3607  elab2g  3611  elrabf  3620  elrab3t  3623  eueq2  3645  eqreu  3664  reu8  3668  ru  3715  sbc6g  3746  sbcieg  3756  sbcied  3761  sbcralt  3805  sbcabel  3811  ss2abdv  3997  rcompleq  4229  sbcel1g  4347  sbcel2  4349  csbnestgfw  4353  csbnestgf  4358  sbccsb2  4368  2nreu  4375  disjpss  4394  sbcssg  4454  2reu4lem  4456  rexsngf  4606  reusngf  4608  ralsng  4609  rexsng  4610  ralprgf  4628  rexprgf  4629  ralprg  4630  reuprg0  4638  difsn  4731  preq2b  4778  opthpr  4782  preqsnd  4789  csbopg  4822  ralunsn  4825  uniprg  4856  csbuni  4870  intprg  4912  dfiin2g  4962  iunxsng  5019  iunxsngf  5021  elpwuni  5034  disjxun  5072  sbcbr12g  5130  opthneg  5396  otthg  5400  copsex2g  5407  opeqsng  5417  snopeqop  5420  brsnop  5436  opelopabt  5445  opelopabga  5446  brabga  5447  opelopabgf  5453  csbmpt12  5470  rbropapd  5477  dfid3  5492  frirr  5566  wereu2  5586  opeliunxp  5654  posn  5672  sosn  5673  frsn  5674  brab2a  5680  opbrop  5684  csbcnvgALT  5793  dmopabelb  5825  elrnmpt1  5867  elrnmptg  5868  opelres  5897  eliniseg2  6014  poleloe  6036  xpdifid  6071  cnvpo  6190  reu3op  6195  elpredgg  6215  frpomin  6243  ordtri4  6303  oneqmini  6317  elsucg  6333  elsuc2g  6334  sbcfung  6458  dffun8  6462  fncnv  6507  fununi  6509  fnssresb  6554  fnimaeq0  6566  csbfv12  6817  dffn5  6828  funimass4  6834  feqmptdf  6839  fnsnfvOLD  6848  dmfco  6864  fndmdif  6919  fvimacnvi  6929  fvimacnvALT  6934  unpreima  6940  respreima  6943  fmptco  7001  fressnfv  7032  fmptsnd  7041  fnnfpeq0  7050  tpres  7076  elunirn  7124  dff13  7128  f12dfv  7145  f13dfv  7146  fliftel  7180  isoini  7209  f1oiso  7222  riotaeqimp  7259  fnbrovb  7324  eloprabga  7382  eloprabgaOLD  7383  resoprab2  7393  elrnmpores  7411  ralrnmpo  7412  ovid  7414  ov  7417  ovg  7437  ofrfval2  7554  dfwe2  7624  ssonprc  7637  ordpwsuc  7662  dfom2  7714  f1oweALT  7815  el2xptp0  7878  releldmdifi  7886  fmpox  7907  ovmptss  7933  1stconst  7940  2ndconst  7941  fnsuppres  8007  suppcoss  8023  brtpos2  8048  mpocurryd  8085  csbfrecsg  8100  dfsmo2  8178  rdglim2  8263  seqomlem2  8282  omeu  8416  oeeui  8433  brdifun  8527  eqerlem  8532  brecop  8599  erovlem  8602  eceqoveq  8611  mapfset  8638  mapsnd  8674  ixpsnval  8688  mptelixpg  8723  xpsnen  8842  xpdom2  8854  omxpenlem  8860  xpf1o  8926  mapunen  8933  onfin  9013  fimaxg  9061  fodomfib  9093  fofinf1o  9094  fipreima  9125  supub  9218  infglb  9249  infglbb  9250  fiming  9257  fiinfg  9258  ordtypecbv  9276  ordtypelem3  9279  ordtypelem9  9285  hartogslem1  9301  wofib  9304  wemapsolem  9309  wemapso2lem  9311  noinfep  9418  cantnf  9451  ttrclselem2  9484  ttrclse  9485  rankbnd2  9627  domtri2  9747  infxpenc2  9778  fseqdom  9782  acni2  9802  dfac9  9892  cfeq0  10012  cfsuc  10013  cflim3  10018  cfslb  10022  cofsmo  10025  enfin2i  10077  isfin3ds  10085  isf33lem  10122  fin1a2lem5  10160  axdc2lem  10204  zorn2g  10259  fodomb  10282  brdom7disj  10287  brdom6disj  10288  iundom2g  10296  cfpwsdom  10340  elgch  10378  fpwwe2cbv  10386  fpwwecbv  10400  pwfseqlem3  10416  pwfseqlem4a  10417  pwfseqlem4  10418  ltpiord  10643  nlt1pi  10662  nqereu  10685  addclprlem1  10772  1idpr  10785  reclem3pr  10805  ltsosr  10850  map2psrpr  10866  supsrlem  10867  axrrecex  10919  xrlenlt  11040  eqlei2  11086  addsubeq4  11236  renegcli  11282  lesub0  11492  wloglei  11507  conjmul  11692  rereccl  11693  infm3  11934  supaddc  11942  supadd  11943  supmul1  11944  supmullem1  11945  supmullem2  11946  supmul  11947  creui  11968  nndiv  12019  elznn0  12334  prime  12401  eqreznegel  12674  zsupss  12677  rebtwnz  12687  negelrp  12763  ltxr  12851  elixx3g  13092  ixxun  13095  ioo0  13104  ico0  13125  ioc0  13126  icc0  13127  difreicc  13216  divelunit  13226  iccf1o  13228  elfz2  13246  fzn  13272  fznn  13324  fzshftral  13344  nelfzo  13392  fzosplitsni  13498  om2uzisoi  13674  rabssnn0fi  13706  mptnn0fsupp  13717  sq11i  13908  hashsdom  14096  fi1uzind  14211  wrdval  14220  csbwrdg  14247  wrd2ind  14436  s2f1o  14629  cjreb  14834  rexfiuz  15059  cau3lem  15066  rlim2  15205  ello12  15225  ello1mpt  15230  elo12  15236  o1lo1  15246  lo1resb  15273  o1resb  15275  o1compt  15296  caucvgb  15391  mertens  15598  ruclem12  15950  divides  15965  dvdsabseq  16022  odd2np1  16050  oddm1even  16052  sumodd  16097  divalgmod  16115  modremain  16117  sadadd2lem2  16157  gcdcllem2  16207  bezoutlem2  16248  bezoutlem3  16249  bezoutlem4  16250  isprm2  16387  isprm3  16388  dvdsnprmd  16395  oddprmdvds  16604  prmreclem2  16618  prmreclem5  16621  prmreclem6  16622  4sqlem2  16650  4sqlem12  16657  vdwmc  16679  vdwpc  16681  vdwlem6  16687  vdwlem10  16691  vdwnn  16699  ramval  16709  0ram  16721  prdsleval  17188  pwsle  17203  imasleval  17252  xpsfrnel2  17275  xpsle  17290  isacs2  17362  mreacs  17367  acsfn  17368  iscatd2  17390  catpropd  17418  ciclcl  17514  cicrcl  17515  isssc  17532  evlfcl  17940  uncfcurf  17957  oduleg  18008  pltval  18050  lublecllem  18078  posglbmo  18130  tosso  18137  oduclatb  18225  odudlatb  18243  isipodrs  18255  gsumvalx  18360  elefmndbas  18512  sgrp2rid2  18565  grplmulf1o  18649  grplactcnv  18678  elnmz  18791  eqgid  18808  isghm  18834  ghmeqker  18861  resscntz  18938  symg1bas  18998  pgrpsubgsymgbi  19016  symgfixelq  19041  f1omvdconj  19054  odmulgeq  19164  sylow3lem3  19234  sylow3lem6  19237  efgval2  19330  efgsdm  19336  efgrelexlema  19355  efgcpbllemb  19361  iscyggen2  19481  cyggenod  19484  gsummptfzcl  19570  eldprd  19607  dprdf11  19626  dprddisj2  19642  pgpfac1lem2  19678  pgpfac1  19683  srg1zr  19765  drngid2  20007  issubrg  20024  sdrgacs  20069  islmod  20127  zndvds  20757  znleval  20762  iunocv  20886  pjfval2  20916  pjdm2  20918  dsmmelbas  20946  ellspd  21009  islindf  21019  islindf4  21045  aspval2  21102  psrbag  21120  cply1coe0bi  21471  istopg  22044  basgen2  22139  isclo  22238  mretopd  22243  isnei  22254  isperf3  22304  restdis  22329  neitr  22331  restcls  22332  restlp  22334  restperf  22335  iscn  22386  iscnp  22388  lmbr2  22410  lmbrf  22411  ordtt1  22530  cmpsub  22551  hauscmplem  22557  cmpfi  22559  dfconn2  22570  1stcelcls  22612  1stccn  22614  nllyi  22626  subislly  22632  dissnlocfin  22680  elkgen  22687  ptpjpre1  22722  ptuni2  22727  ptclsg  22766  ptcnplem  22772  txcn  22777  hausdiag  22796  txhaus  22798  txkgen  22803  xkoptsub  22805  cnmpt21  22822  elqtop  22848  tgqtop  22863  r0cld  22889  elfg  23022  fbasrn  23035  trfil2  23038  trfil3  23039  fin1aufil  23083  elfm2  23099  elfm3  23101  flimopn  23126  fbflim  23127  flfnei  23142  flftg  23147  cnpflf2  23151  txflf  23157  fclsbas  23172  alexsubALTlem4  23201  cnextfvval  23216  snclseqg  23267  tgphaus  23268  tsmsfbas  23279  tsmssubm  23294  utopsnneip  23400  prdsxmetlem  23521  imasdsf1olem  23526  xpsdsval  23534  blres  23584  isxms2  23601  metcnp  23697  txmetcnp  23703  txmetcn  23704  metustel  23706  metuel2  23721  dscopn  23729  isngp4  23768  cnblcld  23938  metnrmlem1a  24021  icoopnst  24102  iocopnst  24103  elpi1  24208  isclmp  24260  isncvsngp  24313  lmmbr2  24423  cfil3i  24433  caucfil  24447  iscmet3  24457  lmclim  24467  metcld2  24471  bcthlem4  24491  minveclem3b  24592  minveclem6  24598  minveclem7  24599  ivthle  24620  ivthle2  24621  evthicc2  24624  ovolfioo  24631  ovolficc  24632  ovolgelb  24644  dyadmax  24762  subopnmbl  24768  ismbf3d  24818  mbfimaopnlem  24819  mbfimaopn2  24821  mbfaddlem  24824  mbfsup  24828  mbfinf  24829  i1f1lem  24853  i1fmulclem  24867  itg1climres  24879  mbfi1fseqlem4  24883  itg2monolem1  24915  itg2gt0  24925  isibl  24930  iblcnlem1  24952  ellimc2  25041  dvcnvrelem1  25181  itgsubst  25213  mdegleb  25229  fta1glem2  25331  quotval  25452  vieta1lem1  25470  vieta1lem2  25471  ulm2  25544  ulmcaulem  25553  ulmcau  25554  radcnvlt1  25577  sineq0  25680  cos11  25689  recosf1o  25691  efopn  25813  cxpeq  25910  mcubic  25997  birthdaylem3  26103  rlimcnp  26115  xrlimcnp  26118  eldmgm  26171  dmgmaddn0  26172  lgamgulmlem6  26183  wilth  26220  isppw  26263  isppw2  26264  mumullem2  26329  sqff1o  26331  dvdsmulf1o  26343  fsumvma  26361  fsumvma2  26362  vmasum  26364  chpchtsum  26367  lgsne0  26483  gausslemma2dlem0i  26512  gausslemma2dlem1a  26513  lgseisenlem2  26524  lgsquadlem1  26528  lgsquadlem2  26529  2lgslem1a  26539  addsq2reu  26588  2sqreu  26604  2sqreunn  26605  2sqreult  26606  2sqreunnlt  26608  dchrmusumlema  26641  rpvmasum2  26660  dchrisum0lema  26662  pntibndlem3  26740  pntlemi  26752  pntleml  26759  pnt3  26760  trgcgrg  26876  tgcgr4  26892  colcom  26919  colrot1  26920  ltgov  26958  hlcomb  26964  lncom  26983  mirreu3  27015  isperp  27073  perpcom  27074  iscgra  27170  isinag  27199  brbtwn  27267  brcgr  27268  brbtwn2  27273  colinearalg  27278  axeuclidlem  27330  axcontlem2  27333  axcontlem4  27335  axcontlem7  27338  elntg2  27353  edgiedgb  27424  isuhgr  27430  isushgr  27431  isupgr  27454  isumgr  27465  isuspgr  27522  isusgr  27523  uhgr0v0e  27605  isfusgrf1  27687  opfusgr  27690  usgr1v0e  27693  dfnbgr3  27705  nbuhgr2vtx1edgb  27719  edgnbusgreu  27734  nbusgredgeu0  27735  isuvtx  27762  cusgruvtxb  27789  cplgr3v  27802  cusgrsizeinds  27819  vtxdg0v  27840  vtxd0nedgb  27855  vtxduhgr0nedg  27859  vtxdusgr0edgnelALT  27863  iswlk  27977  wlk1walk  28006  upgr2wlk  28036  upgristrl  28070  2pthnloop  28099  usgr2pthlem  28131  isclwlke  28145  wl-3xortru  35642  wl-3xorfal  35643  wl-sbrimt  35705  wl-sblimt  35706  wl-sbnf1  35710  wl-mo2df  35725  wl-eudf  35727  wl-mo2t  35730  wl-mo3t  35731  wl-ax11-lem6  35741  wl-dfclab  35747  minregex  41141  cnvcnvintabd  41208  sqrtcvallem1  41239  iunrelexpuztr  41327  brtrclfv2  41335  frege124d  41369  or3or  41631  uneqsn  41633  clsk1independent  41656  ntrclsneine0lem  41674  ntrclsiso  41677  ntrclsk2  41678  ntrclskb  41679  ntrclsk3  41680  ntrclsk13  41681  ntrclsk4  41682  ntrneiel2  41696  ntrneiiso  41701  ntrneikb  41704  ntrneik3  41706  ntrneix3  41707  ntrneik13  41708  ntrneix13  41709  ntrneik4w  41710  k0004lem3  41759