Theorem bitr4di 292

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 227	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	bitrdi 290	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr4g  317  bibi2i  340  mtt  367  nbn2  373  ifptru  1091  3bior1fd  1507  3biant1d  1510  clel4g  3620  eueq3  3672  sbceqal  3803  eqrrabd  4014  n0moeu  4310  sbcel12  4372  sbceqg  4373  sbcne12  4376  reldisj  4409  raldifeq  4452  r19.3rz  4460  eldifpr  4619  reusngf  4635  rexreusng  4640  eldiftp  4648  reusv2lem5  5368  prelpw  5418  otthg  5458  2rbropap  5543  rabxp  5703  pwvrel  5705  ssrel3  5767  elrng  5880  iss  6039  idrefALT  6119  xpcan  6180  xpcan2  6181  dfpo2  6317  ordelpss  6408  fcnvres  6781  dffv3  6904  funimass4  6972  unima  6983  funcnvmpt  7018  fndmdif  7064  fneqeql  7068  funimass3  7076  elrnrexdmb  7114  dff4  7125  fnsnbg  7193  fconst4  7243  elunirn  7278  f12dfv  7304  riota1  7421  riota2df  7423  f1ocnvfv3  7438  eqfnov  7572  elrnmpores  7582  caoftrn  7758  ordsucun  7860  dflim3  7882  dfom2  7903  peano5  7929  reldm  8079  opiota  8095  frxp2  8188  xpord2pred  8189  xpord2indlem  8191  suppssr  8240  mpoxopovel  8265  brtpos  8280  rntpos  8284  ordgt0ge1  8529  ondif2  8538  oelim2  8632  omabs  8688  naddrid  8721  iiner  8838  erinxp  8840  qliftfun  8851  mapdm0  8890  uncf  8919  ordunifi  9309  elfi2  9433  elfiun  9449  fifo  9451  noinfep  9688  cantnflem1  9717  cantnf  9721  rankonidlem  9865  r1pwALT  9887  scottabf  9966  cardalephex  10196  alephinit  10201  cflim2  10368  cfsmolem  10375  compssiso  10479  fin1a2lem11  10515  itunisuc  10524  axdclem  10624  brdom6disj  10638  alephreg  10694  fpwwe2lem8  10750  pwfseqlem3  10772  indpi  11019  nqereu  11041  ordpinq  11055  ltanq  11083  ltmnq  11084  suplem2pr  11165  map2psrpr  11222  ssxr  11406  leltne  11426  ltneg  11843  leneg  11846  suprnub  12309  negiso  12324  elnnnn0  12676  nn0sub  12683  fcdmnn0fsupp  12691  zrevaddcl  12768  znnsub  12769  znn0sub  12770  prime  12807  eluz2  12998  indstr  13070  eluz2b1  13073  qrevaddcl  13126  rpneg  13181  xrleltne  13301  dfle2  13303  dflt2  13304  supxrleub  13483  infxrgelb  13493  ixxin  13520  iccid  13548  elicopnf  13603  iccsplit  13643  fzsplit2  13710  fzsn  13727  fzpr  13740  uzsplit  13757  preduz  13811  fvinim0ffz  13951  injresinj  13953  om2uzf1oi  14123  lt2sqi  14359  le2sqi  14360  hashsdom  14552  hashf1lem1  14627  fz1isolem  14633  prprrab  14645  swrdrn3  14830  ccatlcan  14895  ccatrcan  14896  s3eq3seq  15119  2swrd2eqwrdeq  15135  trclfvcotr  15191  cnpart  15436  limsuplt  15675  rlimresb  15761  mertenslem2  16083  fprod2dlem  16176  sadadd2lem2  16649  saddisjlem  16663  bitsuz  16673  gcddiv  16753  algcvgblem  16781  isprm3  16887  isprm5  16912  prmreclem5  17127  vdwapun  17181  vdwmc2  17186  ramcl  17236  pwsle  17693  ismre  17789  mreacs  17861  acsfn  17862  iscatd2  17884  cidpropd  17913  dfiso2  17976  oppcsect2  17983  isfunc  18068  setcinv  18294  lubeldm  18554  lubval  18557  glbeldm  18567  glbval  18570  tosso  18620  ipodrsfi  18742  acsfiindd  18756  submgmacs  18935  imasmnd2  18997  ismhm0  19014  resmndismnd  19032  submacs  19052  imasgrp2  19294  issubg  19365  resgrpisgrp  19387  subgacs  19400  eqgval  19418  ghmqusnsglem1  19524  ghmquskerlem1  19527  gaorber  19552  symgfix2  19660  psgnran  19759  isslw  19852  sylow2alem2  19862  sylow2a  19863  sylow3lem6  19876  efgcpbllemb  19999  prmcyg  20138  gsum2d2lem  20217  gsumcom2  20219  subgdmdprd  20280  dprd2d2  20290  pgpfac1lem2  20321  pgpfac1lem4  20324  imasrng  20429  imasring  20590  isrnghmmul  20702  isnzr2  20798  isdomn3  20996  drngmulne0  21049  subrgacs  21087  sdrgacs  21088  lssle0  21255  lssacs  21272  lssats2  21305  lvecvsn0  21417  rspsn0  21556  isprmidl  21649  islpir  21682  zndvds  21885  znleval  21890  znleval2  21891  lindsmm  22164  islinds3  22170  islindf4  22174  ismhp3  22493  psdmul  22517  matunitlindflem1  23024  eltg2b  23307  discld  23437  opnssneib  23463  cldlp  23498  restbas  23506  leordtvallem1  23558  leordtvallem2  23559  ssidcn  23603  cnprest2  23638  lmss  23646  perfcls  23713  cmpfi  23756  1stccnp  23811  subislly  23830  hausmapdom  23849  locfindis  23879  iskgen3  23898  kgencn  23905  ptpjpre1  23920  xkoccn  23968  txrest  23980  txlm  23997  txkgen  24001  xkopt  24004  xkoinjcn  24036  imasnopn  24039  imasncld  24040  imasncls  24041  qtopcn  24063  kqfeq  24073  isr0  24086  fbfinnfr  24190  trfbas  24193  fbunfip  24218  ufileu  24268  cfinufil  24277  fmid  24309  txflf  24355  fclsrest  24373  alexsubALT  24400  tsmsres  24493  ucnima  24629  fmucndlem  24639  bldisj  24747  xmeter  24782  elbl4  24912  restmetu  24919  dscopn  24922  bl2ioo  25141  isphtpc  25345  tcphcph  25588  lmmbr2  25610  lmmbrf  25613  iscau2  25628  iscauf  25631  caucfil  25634  metcld  25657  metcld2  25658  bcthlem1  25675  bcthlem4  25678  cldcss2  25793  ovolgelb  25831  ovoliunlem1  25853  ismbfcn  25980  mbfmax  26000  mbfimaopnlem  26006  i1faddlem  26044  i1fmullem  26045  i1fres  26056  i1fpos  26057  itg1climres  26065  xrge0f  26082  itgresr  26129  iblcnlem1  26138  limcun  26245  dvres  26261  mdegmullem  26426  r1pid2  26510  ply1remlem  26513  plyremlem  26655  vieta1  26665  ulmcau  26752  sineq0  26882  coseq1  26883  ang180lem3  27169  cubic  27207  atandm  27234  atandm2  27235  atandm3  27236  rlimcnp  27323  rlimcnp2  27324  vmappw  27473  dchrelbas3  27595  dchrelbas4  27600  dchrsum2  27625  bposlem6  27646  2sqreuopltb  27822  2sqreuopnnltb  27824  dchrisumlem3  27848  pntleml  27968  noetasuplem4  28123  noetainflem4  28127  rightge0  28237  addsrid  28380  negleft  28474  negright  28475  mulsrid  28529  mulsne0bd  28602  oniso  28687  om2noseqf1o  28717  zn0subs  28819  avglts1d  28869  avglts2d  28870  istrkg3ld  28953  tgcgr4  29024  lnrot2  29122  islnopp  29245  islmib  29322  mptelee  29502  brbtwn2  29513  axsegconlem6  29530  axsegcon  29535  ax5seg  29546  axpasch  29549  axeuclid  29571  axcontlem4  29575  elntg2  29593  issubgr  29882  nb3gr2nb  29995  uhgrvd00  30145  isrusgr0  30177  wlkcpr  30239  wlkcomp  30241  upgr2wlk  30277  upgrf1istrl  30316  clwlkcomp  30396  clwlkcompbp  30399  iswwlksnx  30459  wspthsnwspthsnon  30535  wspniunwspnon  30542  2pthon3v  30562  usgr2wspthons3  30586  usgr2wspthon  30587  rusgrnumwwlks  30596  clwlkclwwlklem3  30622  clwlkclwwlk  30623  clwwlknonwwlknonb  30727  0pth  30746  eupth2lem2  30850  vdgn1frgrv2  30927  fusgreg2wsp  30967  clwwlknonclwlknonf1o  30993  dlwwlknondlwlknonf1o  30996  wlkl0  30998  nmoolb  31403  nmlno0lem  31425  ubthlem1  31502  ocsh  31915  shle0  32074  eigrei  32466  adjeu  32521  nmoplb  32539  nmfnlb  32556  eleigvec2  32590  nmlnop0iALT  32627  cnlnadjlem5  32703  adjbdln  32715  jplem2  32901  cvbr2  32915  mdsl2bi  32955  chrelat3  33003  eqelbid  33143  sq2reunnltb  33153  rmounid  33163  nelpr  33199  disjunsn  33260  ofpreima  33331  funcnv5mpt  33333  dfcnv2  33340  suppiniseg  33350  gtiso  33365  fpwrelmap  33395  infxrge0glb  33427  xrdifh  33442  fzsplit3  33455  fzo0opth  33465  toslublem  33603  tosglblem  33605  mgcval  33618  mndlrinvb  33656  xrge0tsmsbi  33705  cntzun  33710  isarchi  33813  dvdsrspss  34012  rspsnasso  34013  lsmsnorb  34016  nsgqusf1olem2  34035  ressply1mon1p  34170  constrfin  34448  smatrcl  34498  ist0cld  34535  rspectopn  34569  zarcls  34576  rhmpreimacnlem  34586  unitdivcld  34603  lmxrge0  34654  isrrext  34702  issibf  35035  eulerpartlemr  35076  eulerpartlemmf  35077  eulerpartlemn  35083  dstfrvunirn  35177  ballotlemfc0  35195  ballotlemfcc  35196  reprsuc  35314  reprpmtf1o  35325  reprdifc  35326  bnj919  35468  bnj976  35478  bnj1542  35557  bnj150  35576  bnj151  35577  bnj607  35616  bnj852  35621  bnj873  35624  bnj938  35637  bnj1171  35700  bnj1388  35733  bnj1489  35756  nummin  35806  dfscott3  35827  usgrgt2cycl  36066  srepdflem1  36085  subfacp1lem3  36114  subfacp1lem5  36116  erdszelem9  36131  kur14  36148  iscvm  36191  satf0op  36309  mclsax  36501  rexxfr3dALT  36571  elintfv  36708  fundmpss  36710  opelco3  36717  dfon2  36732  dfbigcup2  36839  sscoid  36853  funpartfv  36887  dfrdg4  36893  cgr3permute3  36990  segletr  37057  segleantisym  37058  seglelin  37059  nmulrid  37124  fneval  37318  neibastop3  37328  eltail  37340  filnetlem4  37347  mh-infprim2bi  37513  bj-hbntbi  37784  bj-equsvt  37851  bj-sbceqgALT  37992  bj-elinxp  38138  bj-clel3gALT  38154  bj-rest10  38200  bj-0int  38213  qdiffALT  38441  topdifinffinlem  38462  isbasisrelowllem1  38470  isbasisrelowllem2  38471  rdgeqoa  38485  finxpreclem4  38509  finxpsuclem  38512  wl-ifp4impr  38582  wl-1xor  38597  phpreu  38719  cos2h  38726  tan2h  38727  poimirlem16  38746  poimirlem19  38749  poimirlem23  38753  poimirlem24  38754  poimirlem26  38756  poimirlem27  38757  mbfposadd  38777  cnambfre  38778  itg2addnclem  38781  itg2addnc  38784  iblabsnclem  38793  ftc1anclem1  38803  ftc1anclem5  38807  findcard4  38824  caures  38886  heiborlem3  38939  heiborlem10  38946  elghomOLD  39013  divrngidl  39154  eqrelf  39382  brvbrvvdif  39393  elrnres  39402  eldmres3  39407  eldmqsres2  39418  exanres  39425  relcnveq  39452  iss2  39468  ecinn0  39477  raldmqsmo  39487  brxrn2  39508  ecxrn  39530  ecxrn2  39532  disjressuc2  39535  elrelsrel  39566  eldmcoss2  39673  eldm1cossres  39674  elrelscnveq  39752  elcoeleqvrelsrel  39804  brredundsredund  39835  brdmqssqs  39855  cnvepresdmqss  39861  eldmqs1cossres  39868  brerser  39886  erimeq2  39887  eleldisjseldisj  39953  prtlem10  40114  prtlem16  40118  prtlem19  40127  prtex  40129  prter3  40131  islshpat  40266  lcvbr2  40271  lcvbr3  40272  lshpsmreu  40358  isat3  40556  hlrelat5N  40650  islpln5  40784  cdlemblem  41042  paddvaln0N  41050  paddval0  41059  cdlemefrs29bpre1  41646  cdlemefrs29cpre1  41647  cdlemg27b  41945  cdlemg33c  41957  cdlemg33e  41959  diaglbN  42304  cdlemm10N  42367  dicopelval2  42430  dicelval2N  42431  dihopelvalcpre  42497  dihglbcpreN  42549  dih1dimatlem  42578  dihatexv  42587  dvh4dimlem  42692  mapdpglem3  42924  hdmap14lem13  43129  hdmapglem7a  43176  eluzp1  43557  fsuppind  43811  isnacs2  43910  rabrenfdioph  44014  expdiophlem1  44221  pw2f1ocnv  44237  pwfi2f1o  44291  numinfctb  44297  dfacbasgrp  44302  islnr3  44309  onsupneqmaxlim0  44418  onsupnmax  44422  onsupuni  44423  tfsconcatrnss  44544  safesnsupfilb  44611  dfhe3  44967  clsk3nimkb  45232  ntrneiiso  45283  ntrneikb  45286  mnuunid  45453  hashnzfzclim  45498  dvconstbi  45510  sbcoreleleqVD  46032  trfr  46147  permac8prim  46199  rfcnpre3  46255  rfcnpre4  46256  r19.3rzf  46378  cncfshift  47089  stoweidlem59  47274  chnsubseqwl  48094  dfafv23  48528  nelbrnel  48551  elsetpreimafvrab  48681  iccpartiun  48721  prproropf1olem0  48789  prprelb  48803  prprspr2  48805  reuprpr  48810  oddm1evenALTV  48978  oddp1evenALTV  48979  oddprmne2  49018  fpprel  49031  dfvopnbgr2  49156  uhgrimisgrgric  49234  isgrlim  49285  gpg5nbgrvtx03starlem1  49371  gpg5nbgrvtx03starlem3  49373  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem3  49376  iscmgmALT  49526  iscsgrpALT  49528  prelrrx2b  50032  mofeu  50164  iscnrm3  50271  joindm2  50287  meetdm2  50289  oppcendc  50337  0funcg  50405  0funcALT  50408  fucoisfunc2lem2  50694  istermc  50814  functermc2  50849  fulltermc  50851  elpglem2  51085