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  1074  3bior1fd  1477  3biant1d  1480  clel4g  3632  eueq3  3685  sbceqal  3818  eqrrabd  4052  n0moeu  4325  sbcel12  4377  sbceqg  4378  sbcne12  4381  reldisj  4419  raldifeq  4460  r19.3rz  4463  ralf0  4480  eldifpr  4625  reusngf  4641  rexreusng  4646  eldiftp  4654  eqsndOLD  4798  reusv2lem5  5360  prelpw  5409  otthg  5448  2rbropap  5529  rabxp  5689  pwvrel  5691  ssrel3  5752  elrng  5858  iss  6009  idrefALT  6087  xpcan  6152  xpcan2  6153  dfpo2  6272  ordelpss  6363  fcnvres  6740  dffv3  6857  funimass4  6928  unima  6939  fndmdif  7017  fneqeql  7021  funimass3  7029  elrnrexdmb  7065  dff4  7076  fnsnbg  7141  fnsnbOLD  7143  fconst4  7191  elunirn  7228  f12dfv  7251  riota1  7368  riota2df  7370  f1ocnvfv3  7385  eqfnov  7521  elrnmpores  7530  caoftrn  7697  ordsucun  7803  dflim3  7826  dfom2  7847  peano5  7872  opiota  8041  frxp2  8126  xpord2pred  8127  xpord2indlem  8129  suppssr  8177  mpoxopovel  8202  brtpos  8217  rntpos  8221  ordgt0ge1  8460  ondif2  8469  oelim2  8562  omabs  8618  naddrid  8650  iiner  8765  erinxp  8767  qliftfun  8778  mapdm0  8818  ordunifi  9244  elfi2  9372  elfiun  9388  fifo  9390  noinfep  9620  cantnflem1  9649  cantnf  9653  rankonidlem  9788  r1pwALT  9806  pr2nelemOLD  9963  cardalephex  10050  alephinit  10055  dfac5lem4OLD  10088  cflim2  10223  cfsmolem  10230  compssiso  10334  fin1a2lem11  10370  itunisuc  10379  axdclem  10479  brdom6disj  10492  alephreg  10542  fpwwe2lem8  10598  pwfseqlem3  10620  indpi  10867  nqereu  10889  ordpinq  10903  ltanq  10931  ltmnq  10932  suplem2pr  11013  map2psrpr  11070  ssxr  11250  leltne  11270  ltneg  11685  leneg  11688  suprnub  12155  negiso  12170  elnnnn0  12492  nn0sub  12499  fcdmnn0fsupp  12507  zrevaddcl  12585  znnsub  12586  znn0sub  12587  prime  12622  eluz2  12806  indstr  12882  eluz2b1  12885  qrevaddcl  12937  rpneg  12992  xrleltne  13112  dfle2  13114  dflt2  13115  supxrleub  13293  infxrgelb  13303  ixxin  13330  iccid  13358  elicopnf  13413  iccsplit  13453  fzsplit2  13517  fzsn  13534  fzpr  13547  uzsplit  13564  preduz  13618  fvinim0ffz  13754  injresinj  13756  om2uzf1oi  13925  lt2sqi  14161  le2sqi  14162  hashsdom  14353  hashf1lem1  14427  fz1isolem  14433  prprrab  14445  ccatlcan  14690  ccatrcan  14691  s3eq3seq  14912  2swrd2eqwrdeq  14926  trclfvcotr  14982  cnpart  15213  limsuplt  15452  rlimresb  15538  mertenslem2  15858  fprod2dlem  15953  sadadd2lem2  16427  saddisjlem  16441  bitsuz  16451  gcddiv  16528  algcvgblem  16554  isprm3  16660  isprm5  16684  prmreclem5  16898  vdwapun  16952  vdwmc2  16957  ramcl  17007  pwsle  17462  ismre  17558  mreacs  17626  acsfn  17627  iscatd2  17649  cidpropd  17678  dfiso2  17741  oppcsect2  17748  isfunc  17833  setcinv  18059  lubeldm  18319  lubval  18322  glbeldm  18332  glbval  18335  tosso  18385  ipodrsfi  18505  acsfiindd  18519  submgmacs  18651  imasmnd2  18708  ismhm0  18724  resmndismnd  18742  submacs  18761  imasgrp2  18994  issubg  19065  resgrpisgrp  19086  subgacs  19100  eqgval  19116  ghmqusnsglem1  19219  ghmquskerlem1  19222  gaorber  19247  symgfix2  19353  psgnran  19452  isslw  19545  sylow2alem2  19555  sylow2a  19556  sylow3lem6  19569  efgcpbllemb  19692  prmcyg  19831  gsum2d2lem  19910  gsumcom2  19912  subgdmdprd  19973  dprd2d2  19983  pgpfac1lem2  20014  pgpfac1lem4  20017  imasrng  20093  imasring  20246  isrnghmmul  20358  isnzr2  20434  isdomn3  20631  drngmulne0  20678  subrgacs  20716  sdrgacs  20717  lssle0  20863  lssacs  20880  lssats2  20913  lvecvsn0  21026  islpir  21245  zndvds  21466  znleval  21471  znleval2  21472  lindsmm  21744  islinds3  21750  islindf4  21754  ismhp3  22036  psdmul  22060  eltg2b  22853  discld  22983  opnssneib  23009  cldlp  23044  restbas  23052  leordtvallem1  23104  leordtvallem2  23105  ssidcn  23149  cnprest2  23184  lmss  23192  perfcls  23259  cmpfi  23302  1stccnp  23356  subislly  23375  hausmapdom  23394  locfindis  23424  iskgen3  23443  kgencn  23450  ptpjpre1  23465  xkoccn  23513  txrest  23525  txlm  23542  txkgen  23546  xkopt  23549  xkoinjcn  23581  imasnopn  23584  imasncld  23585  imasncls  23586  qtopcn  23608  kqfeq  23618  isr0  23631  fbfinnfr  23735  trfbas  23738  fbunfip  23763  ufileu  23813  cfinufil  23822  fmid  23854  txflf  23900  fclsrest  23918  alexsubALT  23945  tsmsres  24038  ucnima  24175  fmucndlem  24185  bldisj  24293  xmeter  24328  elbl4  24458  restmetu  24465  dscopn  24468  bl2ioo  24687  isphtpc  24900  tcphcph  25144  lmmbr2  25166  lmmbrf  25169  iscau2  25184  iscauf  25187  caucfil  25190  metcld  25213  metcld2  25214  bcthlem1  25231  bcthlem4  25234  cldcss2  25349  ovolgelb  25388  ovoliunlem1  25410  ismbfcn  25537  mbfmax  25557  mbfimaopnlem  25563  i1faddlem  25601  i1fmullem  25602  i1fres  25613  i1fpos  25614  itg1climres  25622  xrge0f  25639  itgresr  25687  iblcnlem1  25696  limcun  25803  dvres  25819  mdegmullem  25990  r1pid2  26074  ply1remlem  26077  plyremlem  26219  vieta1  26227  ulmcau  26311  sineq0  26440  coseq1  26441  ang180lem3  26728  cubic  26766  atandm  26793  atandm2  26794  atandm3  26795  rlimcnp  26882  rlimcnp2  26883  vmappw  27033  dchrelbas3  27156  dchrelbas4  27161  dchrsum2  27186  bposlem6  27207  2sqreuopltb  27383  2sqreuopnnltb  27385  dchrisumlem3  27409  pntleml  27529  noetasuplem4  27655  noetainflem4  27659  addsrid  27878  mulsrid  28023  mulsne0bd  28096  onsiso  28176  om2noseqf1o  28202  zn0subs  28298  istrkg3ld  28395  tgcgr4  28465  lnrot2  28558  islnopp  28673  islmib  28721  brbtwn2  28839  axsegconlem6  28856  axsegcon  28861  ax5seg  28872  axpasch  28875  axeuclid  28897  axcontlem4  28901  elntg2  28919  issubgr  29205  nb3gr2nb  29318  uhgrvd00  29469  isrusgr0  29501  wlkcpr  29564  wlkcomp  29566  upgr2wlk  29603  upgrf1istrl  29638  clwlkcomp  29716  clwlkcompbp  29719  iswwlksnx  29777  wspthsnwspthsnon  29853  wspniunwspnon  29860  2pthon3v  29880  usgr2wspthons3  29901  usgr2wspthon  29902  rusgrnumwwlks  29911  clwlkclwwlklem3  29937  clwlkclwwlk  29938  clwwlknonwwlknonb  30042  0pth  30061  eupth2lem2  30155  vdgn1frgrv2  30232  fusgreg2wsp  30272  clwwlknonclwlknonf1o  30298  dlwwlknondlwlknonf1o  30301  wlkl0  30303  nmoolb  30707  nmlno0lem  30729  ubthlem1  30806  ocsh  31219  shle0  31378  eigrei  31770  adjeu  31825  nmoplb  31843  nmfnlb  31860  eleigvec2  31894  nmlnop0iALT  31931  cnlnadjlem5  32007  adjbdln  32019  jplem2  32205  cvbr2  32219  mdsl2bi  32259  chrelat3  32307  eqelbid  32411  sq2reunnltb  32421  rmounid  32431  nelpr  32467  disjunsn  32530  ofpreima  32596  funcnvmpt  32598  funcnv5mpt  32599  dfcnv2  32607  suppiniseg  32616  gtiso  32631  fpwrelmap  32663  infxrge0glb  32695  xrdifh  32710  fzsplit3  32723  fzo0opth  32735  swrdrn3  32884  toslublem  32905  tosglblem  32907  mgcval  32920  mndlrinvb  32973  xrge0tsmsbi  33010  cntzun  33015  isarchi  33143  dvdsrspss  33365  rspsnasso  33366  lsmsnorb  33369  nsgqusf1olem2  33392  isprmidl  33416  ressply1mon1p  33544  r1pid2OLD  33581  constrfin  33743  smatrcl  33793  ist0cld  33830  rspectopn  33864  zarcls  33871  rhmpreimacnlem  33881  unitdivcld  33898  lmxrge0  33949  isrrext  33997  issibf  34331  eulerpartlemr  34372  eulerpartlemmf  34373  eulerpartlemn  34379  dstfrvunirn  34473  ballotlemfc0  34491  ballotlemfcc  34492  reprsuc  34613  reprpmtf1o  34624  reprdifc  34625  bnj919  34764  bnj976  34774  bnj1542  34854  bnj150  34873  bnj151  34874  bnj607  34913  bnj852  34918  bnj873  34921  bnj938  34934  bnj1171  34997  bnj1388  35030  bnj1489  35053  nummin  35088  usgrgt2cycl  35124  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem9  35193  kur14  35210  iscvm  35253  satf0op  35371  mclsax  35563  rexxfr3dALT  35633  elintfv  35759  fundmpss  35761  opelco3  35769  dfon2  35787  dfbigcup2  35894  sscoid  35908  funpartfv  35940  dfrdg4  35946  cgr3permute3  36042  segletr  36109  segleantisym  36110  seglelin  36111  fneval  36347  neibastop3  36357  eltail  36369  filnetlem4  36376  bj-hbntbi  36699  bj-equsvt  36774  bj-sbceqgALT  36897  bj-clel3gALT  37043  bj-rest10  37083  bj-0int  37096  topdifinffinlem  37342  isbasisrelowllem1  37350  isbasisrelowllem2  37351  rdgeqoa  37365  finxpreclem4  37389  finxpsuclem  37392  wl-ifp4impr  37462  wl-1xor  37477  uncf  37600  phpreu  37605  cos2h  37612  tan2h  37613  matunitlindflem1  37617  poimirlem16  37637  poimirlem19  37640  poimirlem23  37644  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  mbfposadd  37668  cnambfre  37669  itg2addnclem  37672  itg2addnc  37675  iblabsnclem  37684  ftc1anclem1  37694  ftc1anclem5  37698  caures  37761  heiborlem3  37814  heiborlem10  37821  elghomOLD  37888  divrngidl  38029  eqrelf  38251  brvbrvvdif  38260  elrnres  38267  eldmres3  38272  eldmqsres2  38283  exanres  38290  relcnveq  38317  iss2  38333  ecinn0  38342  brxrn2  38364  ecxrn  38380  disjressuc2  38381  eldmcoss2  38457  eldm1cossres  38458  elrelsrel  38485  elrelscnveq  38490  elcoeleqvrelsrel  38594  brredundsredund  38625  brdmqssqs  38645  cnvepresdmqss  38651  eldmqs1cossres  38658  brerser  38676  erimeq2  38677  eleldisjseldisj  38728  prtlem10  38865  prtlem16  38869  prtlem19  38878  prtex  38880  prter3  38882  islshpat  39017  lcvbr2  39022  lcvbr3  39023  lshpsmreu  39109  isat3  39307  hlrelat5N  39402  islpln5  39536  cdlemblem  39794  paddvaln0N  39802  paddval0  39811  cdlemefrs29bpre1  40398  cdlemefrs29cpre1  40399  cdlemg27b  40697  cdlemg33c  40709  cdlemg33e  40711  diaglbN  41056  cdlemm10N  41119  dicopelval2  41182  dicelval2N  41183  dihopelvalcpre  41249  dihglbcpreN  41301  dih1dimatlem  41330  dihatexv  41339  dvh4dimlem  41444  mapdpglem3  41676  hdmap14lem13  41881  hdmapglem7a  41928  eluzp1  42302  fsuppind  42585  isnacs2  42701  rabrenfdioph  42809  expdiophlem1  43017  pw2f1ocnv  43033  pwfi2f1o  43092  numinfctb  43099  dfacbasgrp  43104  islnr3  43111  onsupneqmaxlim0  43220  onsupnmax  43224  onsupuni  43225  tfsconcatrnss  43346  safesnsupfilb  43414  dfhe3  43771  clsk3nimkb  44036  ntrneiiso  44087  ntrneikb  44090  scottabf  44236  mnuunid  44273  hashnzfzclim  44318  dvconstbi  44330  sbcoreleleqVD  44855  trfr  44959  permac8prim  45011  rfcnpre3  45034  rfcnpre4  45035  r19.3rzf  45159  cncfshift  45879  stoweidlem59  46064  dfafv23  47258  nelbrnel  47281  elsetpreimafvrab  47399  iccpartiun  47439  prproropf1olem0  47507  prprelb  47521  prprspr2  47523  reuprpr  47528  oddm1evenALTV  47680  oddp1evenALTV  47681  oddprmne2  47720  fpprel  47733  dfvopnbgr2  47857  uhgrimisgrgric  47935  isgrlim  47985  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  iscmgmALT  48216  iscsgrpALT  48218  mofeu  48840  iscnrm3  48944  joindm2  48960  meetdm2  48962  oppcendc  49011  0funcg  49078  0funcALT  49081  istermc  49467  functermc2  49502  fulltermc  49504  elpglem2  49705