Theorem bitr4di 289

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

Hypotheses

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

Assertion

Ref	Expression
bitr4di	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4di.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 224	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 287	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3bitr4g  314  bibi2i  337  mtt  364  nbn2  370  ifptru  1075  3bior1fd  1478  3biant1d  1481  clel4g  3619  eueq3  3671  sbceqal  3804  eqrrabd  4040  n0moeu  4313  sbcel12  4365  sbceqg  4366  sbcne12  4369  reldisj  4407  raldifeq  4448  r19.3rz  4456  eldifpr  4617  reusngf  4633  rexreusng  4638  eldiftp  4646  eqsndOLD  4789  reusv2lem5  5349  prelpw  5401  otthg  5441  2rbropap  5520  rabxp  5680  pwvrel  5682  ssrel3  5743  elrng  5848  iss  6002  idrefALT  6078  xpcan  6142  xpcan2  6143  dfpo2  6262  ordelpss  6353  fcnvres  6719  dffv3  6838  funimass4  6906  unima  6917  funcnvmpt  6951  fndmdif  6996  fneqeql  7000  funimass3  7008  elrnrexdmb  7044  dff4  7055  fnsnbg  7120  fnsnbOLD  7122  fconst4  7170  elunirn  7207  f12dfv  7229  riota1  7346  riota2df  7348  f1ocnvfv3  7363  eqfnov  7497  elrnmpores  7506  caoftrn  7673  ordsucun  7777  dflim3  7799  dfom2  7820  peano5  7845  opiota  8013  frxp2  8096  xpord2pred  8097  xpord2indlem  8099  suppssr  8147  mpoxopovel  8172  brtpos  8187  rntpos  8191  ordgt0ge1  8430  ondif2  8439  oelim2  8533  omabs  8589  naddrid  8621  iiner  8738  erinxp  8740  qliftfun  8751  mapdm0  8791  ordunifi  9202  elfi2  9329  elfiun  9345  fifo  9347  noinfep  9581  cantnflem1  9610  cantnf  9614  rankonidlem  9752  r1pwALT  9770  cardalephex  10012  alephinit  10017  dfac5lem4OLD  10050  cflim2  10185  cfsmolem  10192  compssiso  10296  fin1a2lem11  10332  itunisuc  10341  axdclem  10441  brdom6disj  10454  alephreg  10505  fpwwe2lem8  10561  pwfseqlem3  10583  indpi  10830  nqereu  10852  ordpinq  10866  ltanq  10894  ltmnq  10895  suplem2pr  10976  map2psrpr  11033  ssxr  11214  leltne  11234  ltneg  11649  leneg  11652  suprnub  12119  negiso  12134  elnnnn0  12456  nn0sub  12463  fcdmnn0fsupp  12471  zrevaddcl  12548  znnsub  12549  znn0sub  12550  prime  12585  eluz2  12769  indstr  12841  eluz2b1  12844  qrevaddcl  12896  rpneg  12951  xrleltne  13071  dfle2  13073  dflt2  13074  supxrleub  13253  infxrgelb  13263  ixxin  13290  iccid  13318  elicopnf  13373  iccsplit  13413  fzsplit2  13477  fzsn  13494  fzpr  13507  uzsplit  13524  preduz  13578  fvinim0ffz  13717  injresinj  13719  om2uzf1oi  13888  lt2sqi  14124  le2sqi  14125  hashsdom  14316  hashf1lem1  14390  fz1isolem  14396  prprrab  14408  ccatlcan  14653  ccatrcan  14654  s3eq3seq  14874  2swrd2eqwrdeq  14888  trclfvcotr  14944  cnpart  15175  limsuplt  15414  rlimresb  15500  mertenslem2  15820  fprod2dlem  15915  sadadd2lem2  16389  saddisjlem  16403  bitsuz  16413  gcddiv  16490  algcvgblem  16516  isprm3  16622  isprm5  16646  prmreclem5  16860  vdwapun  16914  vdwmc2  16919  ramcl  16969  pwsle  17425  ismre  17521  mreacs  17593  acsfn  17594  iscatd2  17616  cidpropd  17645  dfiso2  17708  oppcsect2  17715  isfunc  17800  setcinv  18026  lubeldm  18286  lubval  18289  glbeldm  18299  glbval  18302  tosso  18352  ipodrsfi  18474  acsfiindd  18488  submgmacs  18654  imasmnd2  18711  ismhm0  18727  resmndismnd  18745  submacs  18764  imasgrp2  18997  issubg  19068  resgrpisgrp  19089  subgacs  19102  eqgval  19118  ghmqusnsglem1  19221  ghmquskerlem1  19224  gaorber  19249  symgfix2  19357  psgnran  19456  isslw  19549  sylow2alem2  19559  sylow2a  19560  sylow3lem6  19573  efgcpbllemb  19696  prmcyg  19835  gsum2d2lem  19914  gsumcom2  19916  subgdmdprd  19977  dprd2d2  19987  pgpfac1lem2  20018  pgpfac1lem4  20021  imasrng  20124  imasring  20278  isrnghmmul  20390  isnzr2  20463  isdomn3  20660  drngmulne0  20707  subrgacs  20745  sdrgacs  20746  lssle0  20913  lssacs  20930  lssats2  20963  lvecvsn0  21076  islpir  21295  zndvds  21516  znleval  21521  znleval2  21522  lindsmm  21795  islinds3  21801  islindf4  21805  ismhp3  22097  psdmul  22121  eltg2b  22915  discld  23045  opnssneib  23071  cldlp  23106  restbas  23114  leordtvallem1  23166  leordtvallem2  23167  ssidcn  23211  cnprest2  23246  lmss  23254  perfcls  23321  cmpfi  23364  1stccnp  23418  subislly  23437  hausmapdom  23456  locfindis  23486  iskgen3  23505  kgencn  23512  ptpjpre1  23527  xkoccn  23575  txrest  23587  txlm  23604  txkgen  23608  xkopt  23611  xkoinjcn  23643  imasnopn  23646  imasncld  23647  imasncls  23648  qtopcn  23670  kqfeq  23680  isr0  23693  fbfinnfr  23797  trfbas  23800  fbunfip  23825  ufileu  23875  cfinufil  23884  fmid  23916  txflf  23962  fclsrest  23980  alexsubALT  24007  tsmsres  24100  ucnima  24236  fmucndlem  24246  bldisj  24354  xmeter  24389  elbl4  24519  restmetu  24526  dscopn  24529  bl2ioo  24748  isphtpc  24961  tcphcph  25205  lmmbr2  25227  lmmbrf  25230  iscau2  25245  iscauf  25248  caucfil  25251  metcld  25274  metcld2  25275  bcthlem1  25292  bcthlem4  25295  cldcss2  25410  ovolgelb  25449  ovoliunlem1  25471  ismbfcn  25598  mbfmax  25618  mbfimaopnlem  25624  i1faddlem  25662  i1fmullem  25663  i1fres  25674  i1fpos  25675  itg1climres  25683  xrge0f  25700  itgresr  25748  iblcnlem1  25757  limcun  25864  dvres  25880  mdegmullem  26051  r1pid2  26135  ply1remlem  26138  plyremlem  26280  vieta1  26288  ulmcau  26372  sineq0  26501  coseq1  26502  ang180lem3  26789  cubic  26827  atandm  26854  atandm2  26855  atandm3  26856  rlimcnp  26943  rlimcnp2  26944  vmappw  27094  dchrelbas3  27217  dchrelbas4  27222  dchrsum2  27247  bposlem6  27268  2sqreuopltb  27444  2sqreuopnnltb  27446  dchrisumlem3  27470  pntleml  27590  noetasuplem4  27716  noetainflem4  27720  rightge0  27829  addsrid  27972  negleft  28066  negright  28067  mulsrid  28121  mulsne0bd  28194  oniso  28279  om2noseqf1o  28309  zn0subs  28411  avglts1d  28461  avglts2d  28462  istrkg3ld  28545  tgcgr4  28615  lnrot2  28708  islnopp  28823  islmib  28871  mptelee  28979  brbtwn2  28990  axsegconlem6  29007  axsegcon  29012  ax5seg  29023  axpasch  29026  axeuclid  29048  axcontlem4  29052  elntg2  29070  issubgr  29356  nb3gr2nb  29469  uhgrvd00  29620  isrusgr0  29652  wlkcpr  29714  wlkcomp  29716  upgr2wlk  29752  upgrf1istrl  29787  clwlkcomp  29864  clwlkcompbp  29867  iswwlksnx  29925  wspthsnwspthsnon  30001  wspniunwspnon  30008  2pthon3v  30028  usgr2wspthons3  30052  usgr2wspthon  30053  rusgrnumwwlks  30062  clwlkclwwlklem3  30088  clwlkclwwlk  30089  clwwlknonwwlknonb  30193  0pth  30212  eupth2lem2  30306  vdgn1frgrv2  30383  fusgreg2wsp  30423  clwwlknonclwlknonf1o  30449  dlwwlknondlwlknonf1o  30452  wlkl0  30454  nmoolb  30858  nmlno0lem  30880  ubthlem1  30957  ocsh  31370  shle0  31529  eigrei  31921  adjeu  31976  nmoplb  31994  nmfnlb  32011  eleigvec2  32045  nmlnop0iALT  32082  cnlnadjlem5  32158  adjbdln  32170  jplem2  32356  cvbr2  32370  mdsl2bi  32410  chrelat3  32458  eqelbid  32560  sq2reunnltb  32570  rmounid  32580  nelpr  32617  disjunsn  32680  ofpreima  32754  funcnv5mpt  32756  dfcnv2  32764  suppiniseg  32775  gtiso  32790  fpwrelmap  32822  infxrge0glb  32855  xrdifh  32870  fzsplit3  32883  fzo0opth  32893  swrdrn3  33047  toslublem  33064  tosglblem  33066  mgcval  33079  mndlrinvb  33117  xrge0tsmsbi  33167  cntzun  33172  isarchi  33275  dvdsrspss  33479  rspsnasso  33480  lsmsnorb  33483  nsgqusf1olem2  33506  isprmidl  33530  ressply1mon1p  33660  r1pid2OLD  33701  constrfin  33923  smatrcl  33973  ist0cld  34010  rspectopn  34044  zarcls  34051  rhmpreimacnlem  34061  unitdivcld  34078  lmxrge0  34129  isrrext  34177  issibf  34510  eulerpartlemr  34551  eulerpartlemmf  34552  eulerpartlemn  34558  dstfrvunirn  34652  ballotlemfc0  34670  ballotlemfcc  34671  reprsuc  34792  reprpmtf1o  34803  reprdifc  34804  bnj919  34943  bnj976  34953  bnj1542  35032  bnj150  35051  bnj151  35052  bnj607  35091  bnj852  35096  bnj873  35099  bnj938  35112  bnj1171  35175  bnj1388  35208  bnj1489  35231  nummin  35268  usgrgt2cycl  35343  subfacp1lem3  35395  subfacp1lem5  35397  erdszelem9  35412  kur14  35429  iscvm  35472  satf0op  35590  mclsax  35782  rexxfr3dALT  35852  elintfv  35978  fundmpss  35980  opelco3  35988  dfon2  36003  dfbigcup2  36110  sscoid  36124  funpartfv  36158  dfrdg4  36164  cgr3permute3  36260  segletr  36327  segleantisym  36328  seglelin  36329  fneval  36565  neibastop3  36575  eltail  36587  filnetlem4  36594  bj-hbntbi  36942  bj-equsvt  37005  bj-sbceqgALT  37141  bj-clel3gALT  37287  bj-rest10  37332  bj-0int  37345  topdifinffinlem  37591  isbasisrelowllem1  37599  isbasisrelowllem2  37600  rdgeqoa  37614  finxpreclem4  37638  finxpsuclem  37641  wl-ifp4impr  37711  wl-1xor  37726  uncf  37839  phpreu  37844  cos2h  37851  tan2h  37852  matunitlindflem1  37856  poimirlem16  37876  poimirlem19  37879  poimirlem23  37883  poimirlem24  37884  poimirlem26  37886  poimirlem27  37887  mbfposadd  37907  cnambfre  37908  itg2addnclem  37911  itg2addnc  37914  iblabsnclem  37923  ftc1anclem1  37933  ftc1anclem5  37937  caures  38000  heiborlem3  38053  heiborlem10  38060  elghomOLD  38127  divrngidl  38268  eqrelf  38498  brvbrvvdif  38509  elrnres  38518  eldmres3  38523  eldmqsres2  38534  exanres  38541  relcnveq  38568  iss2  38584  ecinn0  38593  raldmqsmo  38603  brxrn2  38624  ecxrn  38646  ecxrn2  38648  disjressuc2  38651  elrelsrel  38682  eldmcoss2  38789  eldm1cossres  38790  elrelscnveq  38868  elcoeleqvrelsrel  38920  brredundsredund  38951  brdmqssqs  38971  cnvepresdmqss  38977  eldmqs1cossres  38984  brerser  39002  erimeq2  39003  eleldisjseldisj  39069  prtlem10  39230  prtlem16  39234  prtlem19  39243  prtex  39245  prter3  39247  islshpat  39382  lcvbr2  39387  lcvbr3  39388  lshpsmreu  39474  isat3  39672  hlrelat5N  39766  islpln5  39900  cdlemblem  40158  paddvaln0N  40166  paddval0  40175  cdlemefrs29bpre1  40762  cdlemefrs29cpre1  40763  cdlemg27b  41061  cdlemg33c  41073  cdlemg33e  41075  diaglbN  41420  cdlemm10N  41483  dicopelval2  41546  dicelval2N  41547  dihopelvalcpre  41613  dihglbcpreN  41665  dih1dimatlem  41694  dihatexv  41703  dvh4dimlem  41808  mapdpglem3  42040  hdmap14lem13  42245  hdmapglem7a  42292  eluzp1  42666  fsuppind  42937  isnacs2  43052  rabrenfdioph  43160  expdiophlem1  43367  pw2f1ocnv  43383  pwfi2f1o  43442  numinfctb  43449  dfacbasgrp  43454  islnr3  43461  onsupneqmaxlim0  43570  onsupnmax  43574  onsupuni  43575  tfsconcatrnss  43696  safesnsupfilb  43763  dfhe3  44120  clsk3nimkb  44385  ntrneiiso  44436  ntrneikb  44439  scottabf  44585  mnuunid  44622  hashnzfzclim  44667  dvconstbi  44679  sbcoreleleqVD  45203  trfr  45307  permac8prim  45359  rfcnpre3  45382  rfcnpre4  45383  r19.3rzf  45506  cncfshift  46221  stoweidlem59  46406  chnsubseqwl  47226  dfafv23  47602  nelbrnel  47625  elsetpreimafvrab  47743  iccpartiun  47783  prproropf1olem0  47851  prprelb  47865  prprspr2  47867  reuprpr  47872  oddm1evenALTV  48024  oddp1evenALTV  48025  oddprmne2  48064  fpprel  48077  dfvopnbgr2  48202  uhgrimisgrgric  48280  isgrlim  48331  gpg5nbgrvtx03starlem1  48417  gpg5nbgrvtx03starlem3  48419  gpg5nbgrvtx13starlem1  48420  gpg5nbgrvtx13starlem3  48422  iscmgmALT  48573  iscsgrpALT  48575  mofeu  49196  iscnrm3  49300  joindm2  49316  meetdm2  49318  oppcendc  49366  0funcg  49433  0funcALT  49436  istermc  49822  functermc2  49857  fulltermc  49859  elpglem2  50060