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  1476  3biant1d  1479  clel4g  3647  eueq3  3701  sbceqal  3834  eqrrabd  4068  n0moeu  4341  sbcel12  4393  sbceqg  4394  sbcne12  4397  reldisj  4435  raldifeq  4476  r19.3rz  4479  ralf0  4496  eldifpr  4640  reusngf  4656  rexreusng  4661  eldiftp  4669  eqsndOLD  4813  reusv2lem5  5384  prelpw  5433  otthg  5472  2rbropap  5553  rabxp  5715  pwvrel  5717  ssrel3  5778  elrng  5884  iss  6035  idrefALT  6113  xpcan  6178  xpcan2  6179  dfpo2  6298  ordelpss  6393  fcnvres  6766  dffv3  6883  funimass4  6954  unima  6965  fndmdif  7043  fneqeql  7047  funimass3  7055  elrnrexdmb  7091  dff4  7102  fnsnbg  7167  fnsnbOLD  7169  fconst4  7217  elunirn  7254  f12dfv  7276  riota1  7392  riota2df  7394  f1ocnvfv3  7409  eqfnov  7545  elrnmpores  7554  caoftrn  7721  ordsucun  7828  dflim3  7851  dfom2  7872  peano5  7898  opiota  8067  frxp2  8152  xpord2pred  8153  xpord2indlem  8155  suppssr  8203  mpoxopovel  8228  brtpos  8243  rntpos  8247  ordgt0ge1  8514  ondif2  8523  oelim2  8616  omabs  8672  naddrid  8704  iiner  8812  erinxp  8814  qliftfun  8825  mapdm0  8865  ordunifi  9309  elfi2  9437  elfiun  9453  fifo  9455  noinfep  9683  cantnflem1  9712  cantnf  9716  rankonidlem  9851  r1pwALT  9869  pr2nelemOLD  10026  cardalephex  10113  alephinit  10118  dfac5lem4OLD  10151  cflim2  10286  cfsmolem  10293  compssiso  10397  fin1a2lem11  10433  itunisuc  10442  axdclem  10542  brdom6disj  10555  alephreg  10605  fpwwe2lem8  10661  pwfseqlem3  10683  indpi  10930  nqereu  10952  ordpinq  10966  ltanq  10994  ltmnq  10995  suplem2pr  11076  map2psrpr  11133  ssxr  11313  leltne  11333  ltneg  11746  leneg  11749  suprnub  12216  negiso  12231  elnnnn0  12553  nn0sub  12560  fcdmnn0fsupp  12568  zrevaddcl  12646  znnsub  12647  znn0sub  12648  prime  12683  eluz2  12867  indstr  12941  eluz2b1  12944  qrevaddcl  12996  rpneg  13050  xrleltne  13170  dfle2  13172  dflt2  13173  supxrleub  13351  infxrgelb  13360  ixxin  13387  iccid  13415  elicopnf  13468  iccsplit  13508  fzsplit2  13572  fzsn  13589  fzpr  13602  uzsplit  13619  preduz  13673  fvinim0ffz  13808  injresinj  13810  om2uzf1oi  13977  lt2sqi  14211  le2sqi  14212  hashsdom  14403  hashf1lem1  14477  fz1isolem  14483  prprrab  14495  ccatlcan  14739  ccatrcan  14740  s3eq3seq  14961  2swrd2eqwrdeq  14975  trclfvcotr  15031  cnpart  15262  limsuplt  15498  rlimresb  15584  mertenslem2  15904  fprod2dlem  15999  sadadd2lem2  16470  saddisjlem  16484  bitsuz  16494  gcddiv  16571  algcvgblem  16597  isprm3  16703  isprm5  16727  prmreclem5  16941  vdwapun  16995  vdwmc2  17000  ramcl  17050  pwsle  17513  ismre  17609  mreacs  17677  acsfn  17678  iscatd2  17700  cidpropd  17729  dfiso2  17792  oppcsect2  17799  isfunc  17885  setcinv  18111  lubeldm  18372  lubval  18375  glbeldm  18385  glbval  18388  tosso  18438  ipodrsfi  18558  acsfiindd  18572  submgmacs  18704  imasmnd2  18761  ismhm0  18777  resmndismnd  18795  submacs  18814  imasgrp2  19047  issubg  19118  resgrpisgrp  19139  subgacs  19153  eqgval  19169  ghmqusnsglem1  19272  ghmquskerlem1  19275  gaorber  19300  symgfix2  19407  psgnran  19506  isslw  19599  sylow2alem2  19609  sylow2a  19610  sylow3lem6  19623  efgcpbllemb  19746  prmcyg  19885  gsum2d2lem  19964  gsumcom2  19966  subgdmdprd  20027  dprd2d2  20037  pgpfac1lem2  20068  pgpfac1lem4  20071  imasrng  20147  imasring  20300  isrnghmmul  20415  isnzr2  20491  isdomn3  20688  drngmulne0  20735  subrgacs  20774  sdrgacs  20775  lssle0  20921  lssacs  20938  lssats2  20971  lvecvsn0  21084  islpir  21305  zndvds  21535  znleval  21540  znleval2  21541  lindsmm  21815  islinds3  21821  islindf4  21825  ismhp3  22113  psdmul  22137  eltg2b  22932  discld  23062  opnssneib  23088  cldlp  23123  restbas  23131  leordtvallem1  23183  leordtvallem2  23184  ssidcn  23228  cnprest2  23263  lmss  23271  perfcls  23338  cmpfi  23381  1stccnp  23435  subislly  23454  hausmapdom  23473  locfindis  23503  iskgen3  23522  kgencn  23529  ptpjpre1  23544  xkoccn  23592  txrest  23604  txlm  23621  txkgen  23625  xkopt  23628  xkoinjcn  23660  imasnopn  23663  imasncld  23664  imasncls  23665  qtopcn  23687  kqfeq  23697  isr0  23710  fbfinnfr  23814  trfbas  23817  fbunfip  23842  ufileu  23892  cfinufil  23901  fmid  23933  txflf  23979  fclsrest  23997  alexsubALT  24024  tsmsres  24117  ucnima  24254  fmucndlem  24264  bldisj  24372  xmeter  24407  elbl4  24539  restmetu  24546  dscopn  24549  bl2ioo  24768  isphtpc  24981  tcphcph  25226  lmmbr2  25248  lmmbrf  25251  iscau2  25266  iscauf  25269  caucfil  25272  metcld  25295  metcld2  25296  bcthlem1  25313  bcthlem4  25316  cldcss2  25431  ovolgelb  25470  ovoliunlem1  25492  ismbfcn  25619  mbfmax  25639  mbfimaopnlem  25645  i1faddlem  25683  i1fmullem  25684  i1fres  25695  i1fpos  25696  itg1climres  25704  xrge0f  25721  itgresr  25769  iblcnlem1  25778  limcun  25885  dvres  25901  mdegmullem  26072  r1pid2  26156  ply1remlem  26159  plyremlem  26301  vieta1  26309  ulmcau  26393  sineq0  26521  coseq1  26522  ang180lem3  26809  cubic  26847  atandm  26874  atandm2  26875  atandm3  26876  rlimcnp  26963  rlimcnp2  26964  vmappw  27114  dchrelbas3  27237  dchrelbas4  27242  dchrsum2  27267  bposlem6  27288  2sqreuopltb  27464  2sqreuopnnltb  27466  dchrisumlem3  27490  pntleml  27610  noetasuplem4  27736  noetainflem4  27740  addsrid  27952  mulsrid  28094  mulsne0bd  28167  om2noseqf1o  28262  zn0subs  28344  istrkg3ld  28424  tgcgr4  28494  lnrot2  28587  islnopp  28702  islmib  28750  brbtwn2  28869  axsegconlem6  28886  axsegcon  28891  ax5seg  28902  axpasch  28905  axeuclid  28927  axcontlem4  28931  elntg2  28949  issubgr  29235  nb3gr2nb  29348  uhgrvd00  29499  isrusgr0  29531  wlkcpr  29594  wlkcomp  29596  upgr2wlk  29633  upgrf1istrl  29668  clwlkcomp  29746  clwlkcompbp  29749  iswwlksnx  29807  wspthsnwspthsnon  29883  wspniunwspnon  29890  2pthon3v  29910  usgr2wspthons3  29931  usgr2wspthon  29932  rusgrnumwwlks  29941  clwlkclwwlklem3  29967  clwlkclwwlk  29968  clwwlknonwwlknonb  30072  0pth  30091  eupth2lem2  30185  vdgn1frgrv2  30262  fusgreg2wsp  30302  clwwlknonclwlknonf1o  30328  dlwwlknondlwlknonf1o  30331  wlkl0  30333  nmoolb  30737  nmlno0lem  30759  ubthlem1  30836  ocsh  31249  shle0  31408  eigrei  31800  adjeu  31855  nmoplb  31873  nmfnlb  31890  eleigvec2  31924  nmlnop0iALT  31961  cnlnadjlem5  32037  adjbdln  32049  jplem2  32235  cvbr2  32249  mdsl2bi  32289  chrelat3  32337  eqelbid  32441  sq2reunnltb  32451  rmounid  32461  nelpr  32496  disjunsn  32554  ofpreima  32622  funcnvmpt  32624  funcnv5mpt  32625  dfcnv2  32633  suppiniseg  32642  gtiso  32657  fpwrelmap  32691  infxrge0glb  32716  xrdifh  32729  fzsplit3  32742  fzo0opth  32754  swrdrn3  32887  toslublem  32908  tosglblem  32910  mgcval  32923  mndlrinvb  32976  xrge0tsmsbi  33012  cntzun  33017  isarchi  33135  dvdsrspss  33356  rspsnasso  33357  lsmsnorb  33360  nsgqusf1olem2  33383  isprmidl  33407  ressply1mon1p  33534  r1pid2OLD  33570  constrfin  33728  smatrcl  33736  ist0cld  33773  rspectopn  33807  zarcls  33814  rhmpreimacnlem  33824  unitdivcld  33841  lmxrge0  33892  isrrext  33942  issibf  34276  eulerpartlemr  34317  eulerpartlemmf  34318  eulerpartlemn  34324  dstfrvunirn  34418  ballotlemfc0  34436  ballotlemfcc  34437  reprsuc  34571  reprpmtf1o  34582  reprdifc  34583  bnj919  34722  bnj976  34732  bnj1542  34812  bnj150  34831  bnj151  34832  bnj607  34871  bnj852  34876  bnj873  34879  bnj938  34892  bnj1171  34955  bnj1388  34988  bnj1489  35011  nummin  35046  usgrgt2cycl  35076  subfacp1lem3  35128  subfacp1lem5  35130  erdszelem9  35145  kur14  35162  iscvm  35205  satf0op  35323  mclsax  35515  rexxfr3dALT  35585  elintfv  35706  fundmpss  35708  opelco3  35716  dfon2  35734  dfbigcup2  35841  sscoid  35855  funpartfv  35887  dfrdg4  35893  cgr3permute3  35989  segletr  36056  segleantisym  36057  seglelin  36058  fneval  36294  neibastop3  36304  eltail  36316  filnetlem4  36323  bj-hbntbi  36646  bj-equsvt  36721  bj-sbceqgALT  36844  bj-clel3gALT  36990  bj-rest10  37030  bj-0int  37043  topdifinffinlem  37289  isbasisrelowllem1  37297  isbasisrelowllem2  37298  rdgeqoa  37312  finxpreclem4  37336  finxpsuclem  37339  wl-ifp4impr  37409  wl-1xor  37424  uncf  37547  phpreu  37552  cos2h  37559  tan2h  37560  matunitlindflem1  37564  poimirlem16  37584  poimirlem19  37587  poimirlem23  37591  poimirlem24  37592  poimirlem26  37594  poimirlem27  37595  mbfposadd  37615  cnambfre  37616  itg2addnclem  37619  itg2addnc  37622  iblabsnclem  37631  ftc1anclem1  37641  ftc1anclem5  37645  caures  37708  heiborlem3  37761  heiborlem10  37768  elghomOLD  37835  divrngidl  37976  eqrelf  38197  brvbrvvdif  38206  elrnres  38213  eldmqsres2  38230  exanres  38237  relcnveq  38264  iss2  38286  ecinn0  38295  brxrn2  38317  ecxrn  38329  disjressuc2  38330  eldmcoss2  38401  eldm1cossres  38402  elrelsrel  38429  elrelscnveq  38434  elcoeleqvrelsrel  38538  brredundsredund  38569  brdmqssqs  38589  cnvepresdmqss  38594  eldmqs1cossres  38601  brerser  38619  erimeq2  38620  eleldisjseldisj  38671  prtlem10  38807  prtlem16  38811  prtlem19  38820  prtex  38822  prter3  38824  islshpat  38959  lcvbr2  38964  lcvbr3  38965  lshpsmreu  39051  isat3  39249  hlrelat5N  39344  islpln5  39478  cdlemblem  39736  paddvaln0N  39744  paddval0  39753  cdlemefrs29bpre1  40340  cdlemefrs29cpre1  40341  cdlemg27b  40639  cdlemg33c  40651  cdlemg33e  40653  diaglbN  40998  cdlemm10N  41061  dicopelval2  41124  dicelval2N  41125  dihopelvalcpre  41191  dihglbcpreN  41243  dih1dimatlem  41272  dihatexv  41281  dvh4dimlem  41386  mapdpglem3  41618  hdmap14lem13  41823  hdmapglem7a  41870  eluzp1  42286  fsuppind  42545  isnacs2  42662  rabrenfdioph  42770  expdiophlem1  42978  pw2f1ocnv  42994  pwfi2f1o  43053  numinfctb  43060  dfacbasgrp  43065  islnr3  43072  onsupneqmaxlim0  43181  onsupnmax  43185  onsupuni  43186  tfsconcatrnss  43308  safesnsupfilb  43376  dfhe3  43733  clsk3nimkb  43998  ntrneiiso  44049  ntrneikb  44052  scottabf  44204  mnuunid  44241  hashnzfzclim  44286  dvconstbi  44298  sbcoreleleqVD  44824  trfr  44924  rfcnpre3  44983  rfcnpre4  44984  r19.3rzf  45108  cncfshift  45834  stoweidlem59  46019  dfafv23  47211  nelbrnel  47234  elsetpreimafvrab  47327  iccpartiun  47367  prproropf1olem0  47435  prprelb  47449  prprspr2  47451  reuprpr  47456  oddm1evenALTV  47608  oddp1evenALTV  47609  oddprmne2  47648  fpprel  47661  dfvopnbgr2  47785  uhgrimisgrgric  47845  isgrlim  47895  gpg5nbgrvtx03starlem1  47970  gpg5nbgrvtx03starlem3  47972  gpg5nbgrvtx13starlem1  47973  gpg5nbgrvtx13starlem3  47975  iscmgmALT  48086  iscsgrpALT  48088  mofeu  48703  iscnrm3  48797  joindm2  48813  meetdm2  48815  oppcendc  48862  0funcg  48875  0funcALT  48878  istermc  49087  functermc2  49110  fulltermc  49112  elpglem2  49227