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  1475  3biant1d  1478  clel4g  3676  eueq3  3733  sbceqal  3870  eqrrabd  4109  n0moeu  4382  sbcel12  4434  sbceqg  4435  sbcne12  4438  reldisj  4476  raldifeq  4517  r19.3rz  4520  ralf0  4537  eldifpr  4680  reusngf  4696  rexreusng  4703  eldiftp  4710  eqsndOLD  4856  reusv2lem5  5420  prelpw  5466  otthg  5505  2rbropap  5585  rabxp  5748  pwvrel  5750  ssrel3  5810  elrng  5916  iss  6064  idrefALT  6143  xpcan  6207  xpcan2  6208  dfpo2  6327  ordelpss  6423  fcnvres  6798  dffv3  6916  funimass4  6986  unima  6997  fndmdif  7075  fneqeql  7079  funimass3  7087  elrnrexdmb  7124  dff4  7135  fnsnb  7200  fconst4  7251  elunirn  7288  f12dfv  7309  riota1  7426  riota2df  7428  f1ocnvfv3  7443  eqfnov  7579  elrnmpores  7588  caoftrn  7753  ordsucun  7861  dflim3  7884  dfom2  7905  peano5  7932  peano5OLD  7933  opiota  8100  frxp2  8185  xpord2pred  8186  xpord2indlem  8188  suppssr  8236  mpoxopovel  8261  brtpos  8276  rntpos  8280  ordgt0ge1  8549  ondif2  8558  oelim2  8651  omabs  8707  naddrid  8739  iiner  8847  erinxp  8849  qliftfun  8860  mapdm0  8900  ordunifi  9354  elfi2  9483  elfiun  9499  fifo  9501  noinfep  9729  cantnflem1  9758  cantnf  9762  rankonidlem  9897  r1pwALT  9915  pr2nelemOLD  10072  cardalephex  10159  alephinit  10164  dfac5lem4OLD  10197  cflim2  10332  cfsmolem  10339  compssiso  10443  fin1a2lem11  10479  itunisuc  10488  axdclem  10588  brdom6disj  10601  alephreg  10651  fpwwe2lem8  10707  pwfseqlem3  10729  indpi  10976  nqereu  10998  ordpinq  11012  ltanq  11040  ltmnq  11041  suplem2pr  11122  map2psrpr  11179  ssxr  11359  leltne  11379  ltneg  11790  leneg  11793  suprnub  12260  negiso  12275  elnnnn0  12596  nn0sub  12603  fcdmnn0fsupp  12610  zrevaddcl  12688  znnsub  12689  znn0sub  12690  prime  12724  eluz2  12909  indstr  12981  eluz2b1  12984  qrevaddcl  13036  rpneg  13089  xrleltne  13207  dfle2  13209  dflt2  13210  supxrleub  13388  infxrgelb  13397  ixxin  13424  iccid  13452  elicopnf  13505  iccsplit  13545  fzsplit2  13609  fzsn  13626  fzpr  13639  uzsplit  13656  preduz  13707  fvinim0ffz  13836  injresinj  13838  om2uzf1oi  14004  lt2sqi  14238  le2sqi  14239  hashsdom  14430  hashf1lem1  14504  fz1isolem  14510  prprrab  14522  ccatlcan  14766  ccatrcan  14767  s3eq3seq  14988  2swrd2eqwrdeq  15002  trclfvcotr  15058  cnpart  15289  limsuplt  15525  rlimresb  15611  mertenslem2  15933  fprod2dlem  16028  sadadd2lem2  16496  saddisjlem  16510  bitsuz  16520  gcddiv  16598  algcvgblem  16624  isprm3  16730  isprm5  16754  prmreclem5  16967  vdwapun  17021  vdwmc2  17026  ramcl  17076  pwsle  17552  ismre  17648  mreacs  17716  acsfn  17717  iscatd2  17739  cidpropd  17768  dfiso2  17833  oppcsect2  17840  isfunc  17928  setcinv  18157  lubeldm  18423  lubval  18426  glbeldm  18436  glbval  18439  tosso  18489  ipodrsfi  18609  acsfiindd  18623  submgmacs  18755  imasmnd2  18809  ismhm0  18825  resmndismnd  18843  submacs  18862  imasgrp2  19095  issubg  19166  resgrpisgrp  19187  subgacs  19201  eqgval  19217  ghmqusnsglem1  19320  ghmquskerlem1  19323  gaorber  19348  symgfix2  19458  psgnran  19557  isslw  19650  sylow2alem2  19660  sylow2a  19661  sylow3lem6  19674  efgcpbllemb  19797  prmcyg  19936  gsum2d2lem  20015  gsumcom2  20017  subgdmdprd  20078  dprd2d2  20088  pgpfac1lem2  20119  pgpfac1lem4  20122  imasrng  20204  imasring  20353  isrnghmmul  20468  isnzr2  20544  isdomn3  20737  drngmulne0  20784  subrgacs  20823  sdrgacs  20824  lssle0  20971  lssacs  20988  lssats2  21021  lvecvsn0  21134  islpir  21361  zndvds  21591  znleval  21596  znleval2  21597  lindsmm  21871  islinds3  21877  islindf4  21881  ismhp3  22169  psdmul  22193  eltg2b  22987  discld  23118  opnssneib  23144  cldlp  23179  restbas  23187  leordtvallem1  23239  leordtvallem2  23240  ssidcn  23284  cnprest2  23319  lmss  23327  perfcls  23394  cmpfi  23437  1stccnp  23491  subislly  23510  hausmapdom  23529  locfindis  23559  iskgen3  23578  kgencn  23585  ptpjpre1  23600  xkoccn  23648  txrest  23660  txlm  23677  txkgen  23681  xkopt  23684  xkoinjcn  23716  imasnopn  23719  imasncld  23720  imasncls  23721  qtopcn  23743  kqfeq  23753  isr0  23766  fbfinnfr  23870  trfbas  23873  fbunfip  23898  ufileu  23948  cfinufil  23957  fmid  23989  txflf  24035  fclsrest  24053  alexsubALT  24080  tsmsres  24173  ucnima  24311  fmucndlem  24321  bldisj  24429  xmeter  24464  elbl4  24597  restmetu  24604  dscopn  24607  bl2ioo  24833  isphtpc  25045  tcphcph  25290  lmmbr2  25312  lmmbrf  25315  iscau2  25330  iscauf  25333  caucfil  25336  metcld  25359  metcld2  25360  bcthlem1  25377  bcthlem4  25380  cldcss2  25495  ovolgelb  25534  ovoliunlem1  25556  ismbfcn  25683  mbfmax  25703  mbfimaopnlem  25709  i1faddlem  25747  i1fmullem  25748  i1fres  25760  i1fpos  25761  itg1climres  25769  xrge0f  25786  itgresr  25834  iblcnlem1  25843  limcun  25950  dvres  25966  mdegmullem  26137  r1pid2  26221  ply1remlem  26224  plyremlem  26364  vieta1  26372  ulmcau  26456  sineq0  26584  coseq1  26585  ang180lem3  26872  cubic  26910  atandm  26937  atandm2  26938  atandm3  26939  rlimcnp  27026  rlimcnp2  27027  vmappw  27177  dchrelbas3  27300  dchrelbas4  27305  dchrsum2  27330  bposlem6  27351  2sqreuopltb  27527  2sqreuopnnltb  27529  dchrisumlem3  27553  pntleml  27673  noetasuplem4  27799  noetainflem4  27803  addsrid  28015  mulsrid  28157  mulsne0bd  28230  om2noseqf1o  28325  zn0subs  28407  istrkg3ld  28487  tgcgr4  28557  lnrot2  28650  islnopp  28765  islmib  28813  brbtwn2  28938  axsegconlem6  28955  axsegcon  28960  ax5seg  28971  axpasch  28974  axeuclid  28996  axcontlem4  29000  elntg2  29018  issubgr  29306  nb3gr2nb  29419  uhgrvd00  29570  isrusgr0  29602  wlkcpr  29665  wlkcomp  29667  upgr2wlk  29704  upgrf1istrl  29739  clwlkcomp  29815  clwlkcompbp  29818  iswwlksnx  29873  wspthsnwspthsnon  29949  wspniunwspnon  29956  2pthon3v  29976  usgr2wspthons3  29997  usgr2wspthon  29998  rusgrnumwwlks  30007  clwlkclwwlklem3  30033  clwlkclwwlk  30034  clwwlknonwwlknonb  30138  0pth  30157  eupth2lem2  30251  vdgn1frgrv2  30328  fusgreg2wsp  30368  clwwlknonclwlknonf1o  30394  dlwwlknondlwlknonf1o  30397  wlkl0  30399  nmoolb  30803  nmlno0lem  30825  ubthlem1  30902  ocsh  31315  shle0  31474  eigrei  31866  adjeu  31921  nmoplb  31939  nmfnlb  31956  eleigvec2  31990  nmlnop0iALT  32027  cnlnadjlem5  32103  adjbdln  32115  jplem2  32301  cvbr2  32315  mdsl2bi  32355  chrelat3  32403  eqelbid  32503  sq2reunnltb  32513  rmounid  32523  nelpr  32559  disjunsn  32616  ofpreima  32683  funcnvmpt  32685  funcnv5mpt  32686  dfcnv2  32694  suppiniseg  32698  gtiso  32712  fpwrelmap  32747  infxrge0glb  32772  xrdifh  32785  fzsplit3  32799  fzo0opth  32810  swrdrn3  32922  toslublem  32945  tosglblem  32947  mgcval  32960  mndlrinvb  33011  xrge0tsmsbi  33042  cntzun  33044  isarchi  33162  dvdsrspss  33380  rspsnasso  33381  lsmsnorb  33384  nsgqusf1olem2  33407  isprmidl  33431  ressply1mon1p  33558  r1pid2OLD  33594  constrfin  33736  smatrcl  33742  ist0cld  33779  rspectopn  33813  zarcls  33820  rhmpreimacnlem  33830  unitdivcld  33847  lmxrge0  33898  isrrext  33946  issibf  34298  eulerpartlemr  34339  eulerpartlemmf  34340  eulerpartlemn  34346  dstfrvunirn  34439  ballotlemfc0  34457  ballotlemfcc  34458  reprsuc  34592  reprpmtf1o  34603  reprdifc  34604  bnj919  34743  bnj976  34753  bnj1542  34833  bnj150  34852  bnj151  34853  bnj607  34892  bnj852  34897  bnj873  34900  bnj938  34913  bnj1171  34976  bnj1388  35009  bnj1489  35032  nummin  35067  usgrgt2cycl  35098  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem9  35167  kur14  35184  iscvm  35227  satf0op  35345  mclsax  35537  rexxfr3dALT  35607  elintfv  35728  fundmpss  35730  opelco3  35738  dfon2  35756  dfbigcup2  35863  sscoid  35877  funpartfv  35909  dfrdg4  35915  cgr3permute3  36011  segletr  36078  segleantisym  36079  seglelin  36080  fneval  36318  neibastop3  36328  eltail  36340  filnetlem4  36347  bj-hbntbi  36670  bj-equsvt  36745  bj-sbceqgALT  36868  bj-clel3gALT  37014  bj-rest10  37054  bj-0int  37067  topdifinffinlem  37313  isbasisrelowllem1  37321  isbasisrelowllem2  37322  rdgeqoa  37336  finxpreclem4  37360  finxpsuclem  37363  wl-ifp4impr  37433  wl-1xor  37448  uncf  37559  phpreu  37564  cos2h  37571  tan2h  37572  matunitlindflem1  37576  poimirlem16  37596  poimirlem19  37599  poimirlem23  37603  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  mbfposadd  37627  cnambfre  37628  itg2addnclem  37631  itg2addnc  37634  iblabsnclem  37643  ftc1anclem1  37653  ftc1anclem5  37657  caures  37720  heiborlem3  37773  heiborlem10  37780  elghomOLD  37847  divrngidl  37988  eqrelf  38211  brvbrvvdif  38220  elrnres  38227  eldmqsres2  38244  exanres  38251  relcnveq  38278  iss2  38300  ecinn0  38309  brxrn2  38331  ecxrn  38343  disjressuc2  38344  eldmcoss2  38415  eldm1cossres  38416  elrelsrel  38443  elrelscnveq  38448  elcoeleqvrelsrel  38552  brredundsredund  38583  brdmqssqs  38603  cnvepresdmqss  38608  eldmqs1cossres  38615  brerser  38633  erimeq2  38634  eleldisjseldisj  38685  prtlem10  38821  prtlem16  38825  prtlem19  38834  prtex  38836  prter3  38838  islshpat  38973  lcvbr2  38978  lcvbr3  38979  lshpsmreu  39065  isat3  39263  hlrelat5N  39358  islpln5  39492  cdlemblem  39750  paddvaln0N  39758  paddval0  39767  cdlemefrs29bpre1  40354  cdlemefrs29cpre1  40355  cdlemg27b  40653  cdlemg33c  40665  cdlemg33e  40667  diaglbN  41012  cdlemm10N  41075  dicopelval2  41138  dicelval2N  41139  dihopelvalcpre  41205  dihglbcpreN  41257  dih1dimatlem  41286  dihatexv  41295  dvh4dimlem  41400  mapdpglem3  41632  hdmap14lem13  41837  hdmapglem7a  41884  fnsnbt  42225  eluzp1  42295  fsuppind  42545  isnacs2  42662  rabrenfdioph  42770  expdiophlem1  42978  pw2f1ocnv  42994  pwfi2f1o  43053  numinfctb  43060  dfacbasgrp  43065  islnr3  43072  onsupneqmaxlim0  43185  onsupnmax  43189  onsupuni  43190  tfsconcatrnss  43312  safesnsupfilb  43380  dfhe3  43737  clsk3nimkb  44002  ntrneiiso  44053  ntrneikb  44056  scottabf  44209  mnuunid  44246  hashnzfzclim  44291  dvconstbi  44303  sbcoreleleqVD  44830  rfcnpre3  44933  rfcnpre4  44934  r19.3rzf  45063  cncfshift  45795  stoweidlem59  45980  dfafv23  47168  nelbrnel  47191  elsetpreimafvrab  47268  iccpartiun  47308  prproropf1olem0  47376  prprelb  47390  prprspr2  47392  reuprpr  47397  oddm1evenALTV  47549  oddp1evenALTV  47550  oddprmne2  47589  fpprel  47602  dfvopnbgr2  47725  uhgrimisgrgric  47783  isgrlim  47806  iscmgmALT  47947  iscsgrpALT  47949  mofeu  48561  iscnrm3  48632  joindm2  48648  meetdm2  48650  elpglem2  48804