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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3bitr4g  317  bibi2i  341  mtt  368  nbn2  374  ifptru  1071  3bior1fd  1472  3biant1d  1475  clelabOLD  2896  clel4g  3577  eueq3  3627  n0moeu  4257  sbcel12  4308  sbceqg  4309  sbcne12  4312  reldisj  4351  reldisjOLD  4352  raldifeq  4390  r19.3rz  4393  ralf0  4409  eldifpr  4557  reusngf  4572  rexreusng  4577  eldiftp  4584  reusv2lem5  5274  prelpw  5310  otthg  5348  2rbropap  5424  rabxp  5573  pwvrel  5575  elrng  5736  iss  5879  elimasni  5932  eliniseg  5934  idrefALT  5949  xpcan  6009  xpcan2  6010  elpredg  6144  ordelpss  6201  fcnvres  6545  dffv3  6658  funimass4  6722  unima  6731  fndmdif  6807  fneqeql  6811  funimass3  6819  elrnrexdmb  6852  dff4  6863  fnsnb  6924  fconst4  6973  elunirn  7007  f12dfv  7027  riota1  7134  riota2df  7136  f1ocnvfv3  7151  eqfnov  7280  elrnmpores  7288  caoftrn  7447  ordsucun  7544  dflim3  7566  dfom2  7586  peano5  7609  opiota  7766  suppssr  7875  mpoxopovel  7901  brtpos  7916  rntpos  7920  ordgt0ge1  8137  ondif2  8142  oelim2  8236  omabs  8289  iiner  8384  erinxp  8386  qliftfun  8397  mapdm0  8436  ordunifi  8806  elfi2  8916  elfiun  8932  fifo  8934  noinfep  9161  cantnflem1  9190  cantnf  9194  rankonidlem  9295  r1pwALT  9313  pr2nelem  9469  cardalephex  9555  alephinit  9560  dfac5lem4  9591  cflim2  9728  cfsmolem  9735  compssiso  9839  fin1a2lem11  9875  itunisuc  9884  axdclem  9984  brdom6disj  9997  alephreg  10047  fpwwe2lem8  10103  pwfseqlem3  10125  pwfseqlem4  10127  indpi  10372  nqereu  10394  ordpinq  10408  ltanq  10436  ltmnq  10437  suplem2pr  10518  map2psrpr  10575  ssxr  10753  leltne  10773  ltneg  11183  leneg  11186  suprnub  11647  negiso  11662  elnnnn0  11982  nn0sub  11989  frnnn0fsupp  11996  zrevaddcl  12071  znnsub  12072  znn0sub  12073  prime  12107  eluz2  12293  indstr  12361  eluz2b1  12364  qrevaddcl  12416  rpneg  12467  xrleltne  12584  dfle2  12586  dflt2  12587  supxrleub  12765  infxrgelb  12774  ixxin  12801  iccid  12829  elicopnf  12882  iccsplit  12922  fzsplit2  12986  fzsn  13003  fzpr  13016  uzsplit  13033  preduz  13083  fvinim0ffz  13210  injresinj  13212  om2uzf1oi  13375  lt2sqi  13607  le2sqi  13608  hashsdom  13797  hashf1lem1  13869  hashf1lem1OLD  13870  fz1isolem  13876  prprrab  13888  ccatlcan  14132  ccatrcan  14133  s3eq3seq  14353  2swrd2eqwrdeq  14367  trclfvcotr  14421  cnpart  14652  limsuplt  14889  rlimresb  14975  mertenslem2  15294  fprod2dlem  15387  sadadd2lem2  15854  saddisjlem  15868  bitsuz  15878  gcddiv  15955  algcvgblem  15978  isprm3  16084  isprm5  16108  prmreclem5  16316  vdwapun  16370  vdwmc2  16375  ramcl  16425  pwsle  16828  ismre  16924  mreacs  16992  acsfn  16993  iscatd2  17015  cidpropd  17043  dfiso2  17106  oppcsect2  17113  isfunc  17198  setcinv  17421  lubeldm  17662  lubval  17665  glbeldm  17675  glbval  17678  tosso  17717  ipodrsfi  17844  acsfiindd  17858  imasmnd2  18019  resmndismnd  18044  submacs  18062  imasgrp2  18286  issubg  18351  resgrpisgrp  18372  subgacs  18385  eqgval  18401  gaorber  18510  symgfix2  18616  psgnran  18715  isslw  18805  sylow2alem2  18815  sylow2a  18816  sylow3lem6  18829  efgcpbllemb  18953  prmcyg  19087  gsum2d2lem  19166  gsumcom2  19168  subgdmdprd  19229  dprd2d2  19239  pgpfac1lem2  19270  pgpfac1lem4  19273  imasring  19445  drngmulne0  19597  subrgacs  19652  sdrgacs  19653  lssle0  19794  lssacs  19812  lssats2  19845  lvecvsn0  19954  islpir  20095  isnzr2  20109  zndvds  20322  znleval  20327  znleval2  20328  lindsmm  20598  islinds3  20604  islindf4  20608  ismhp3  20891  eltg2b  21664  discld  21794  opnssneib  21820  cldlp  21855  restbas  21863  leordtvallem1  21915  leordtvallem2  21916  ssidcn  21960  cnprest2  21995  lmss  22003  perfcls  22070  cmpfi  22113  1stccnp  22167  subislly  22186  hausmapdom  22205  locfindis  22235  iskgen3  22254  kgencn  22261  ptpjpre1  22276  xkoccn  22324  txrest  22336  txlm  22353  txkgen  22357  xkopt  22360  xkoinjcn  22392  imasnopn  22395  imasncld  22396  imasncls  22397  qtopcn  22419  kqfeq  22429  isr0  22442  fbfinnfr  22546  trfbas  22549  fbunfip  22574  ufileu  22624  cfinufil  22633  fmid  22665  txflf  22711  fclsrest  22729  alexsubALT  22756  tsmsres  22849  ucnima  22987  fmucndlem  22997  bldisj  23105  xmeter  23140  elbl4  23270  restmetu  23277  dscopn  23280  bl2ioo  23498  isphtpc  23700  tcphcph  23942  lmmbr2  23964  lmmbrf  23967  iscau2  23982  iscauf  23985  caucfil  23988  metcld  24011  metcld2  24012  bcthlem1  24029  bcthlem4  24032  cldcss2  24147  ovolgelb  24185  ovoliunlem1  24207  ismbfcn  24334  mbfmax  24354  mbfimaopnlem  24360  i1faddlem  24398  i1fmullem  24399  i1fres  24410  i1fpos  24411  itg1climres  24419  xrge0f  24436  itgresr  24483  iblcnlem1  24492  limcun  24599  dvres  24615  mdegmullem  24783  ply1remlem  24867  plyremlem  25004  vieta1  25012  ulmcau  25094  sineq0  25220  coseq1  25221  ang180lem3  25501  cubic  25539  atandm  25566  atandm2  25567  atandm3  25568  rlimcnp  25655  rlimcnp2  25656  vmappw  25805  dchrelbas3  25926  dchrelbas4  25931  dchrsum2  25956  bposlem6  25977  2sqreuopltb  26153  2sqreuopnnltb  26155  dchrisumlem3  26179  pntleml  26299  istrkg3ld  26359  tgcgr4  26429  lnrot2  26522  islnopp  26637  islmib  26685  brbtwn2  26803  axsegconlem6  26820  axsegcon  26825  ax5seg  26836  axpasch  26839  axeuclid  26861  axcontlem4  26865  elntg2  26883  issubgr  27165  nb3gr2nb  27278  uhgrvd00  27428  isrusgr0  27460  wlkcpr  27522  wlkcomp  27524  upgr2wlk  27562  upgrf1istrl  27597  clwlkcomp  27672  clwlkcompbp  27675  iswwlksnx  27730  wspthsnwspthsnon  27806  wspniunwspnon  27813  2pthon3v  27833  usgr2wspthons3  27854  usgr2wspthon  27855  rusgrnumwwlks  27864  clwlkclwwlklem3  27890  clwlkclwwlk  27891  clwwlknonwwlknonb  27995  0pth  28014  eupth2lem2  28108  vdgn1frgrv2  28185  fusgreg2wsp  28225  clwwlknonclwlknonf1o  28251  dlwwlknondlwlknonf1o  28254  wlkl0  28256  nmoolb  28658  nmlno0lem  28680  ubthlem1  28757  ocsh  29170  shle0  29329  eigrei  29721  adjeu  29776  nmoplb  29794  nmfnlb  29811  eleigvec2  29845  nmlnop0iALT  29882  cnlnadjlem5  29958  adjbdln  29970  jplem2  30156  cvbr2  30170  mdsl2bi  30210  chrelat3  30258  sq2reunnltb  30359  rmounid  30370  eqrrabd  30376  eqsnd  30404  nelpr  30406  disjunsn  30460  ofpreima  30530  funcnvmpt  30532  funcnv5mpt  30533  dfcnv2  30541  suppiniseg  30548  gtiso  30561  fpwrelmap  30596  infxrge0glb  30616  xrdifh  30629  fzsplit3  30643  swrdrn3  30755  toslublem  30780  tosglblem  30782  mgcval  30795  xrge0tsmsbi  30848  cntzun  30850  isarchi  30966  lsmsnorb  31104  nsgqusf1olem2  31124  isprmidl  31138  smatrcl  31271  ist0cld  31308  rspectopn  31342  zarcls  31349  rhmpreimacnlem  31359  unitdivcld  31376  lmxrge0  31427  isrrext  31473  issibf  31823  eulerpartlemr  31864  eulerpartlemmf  31865  eulerpartlemn  31871  dstfrvunirn  31964  ballotlemfc0  31982  ballotlemfcc  31983  reprsuc  32118  reprpmtf1o  32129  reprdifc  32130  bnj919  32270  bnj976  32281  bnj1542  32361  bnj150  32380  bnj151  32381  bnj607  32420  bnj852  32425  bnj873  32428  bnj938  32441  bnj1171  32504  bnj1388  32537  bnj1489  32560  nummin  32587  usgrgt2cycl  32612  subfacp1lem3  32664  subfacp1lem5  32666  erdszelem9  32681  kur14  32698  iscvm  32741  satf0op  32859  mclsax  33051  dfpo2  33242  elintfv  33258  fundmpss  33260  opelco3  33269  dfon2  33288  frxp2  33350  xpord2pred  33351  xpord2ind  33353  xpord3ind  33359  naddid1  33425  noetasuplem4  33528  noetainflem4  33532  addsid1  33702  dfbigcup2  33776  sscoid  33790  funpartfv  33822  dfrdg4  33828  cgr3permute3  33924  segletr  33991  segleantisym  33992  seglelin  33993  fneval  34116  neibastop3  34126  eltail  34138  filnetlem4  34145  bj-hbntbi  34458  bj-sbceqgALT  34649  bj-clel3gALT  34773  bj-rest10  34809  bj-0int  34822  topdifinffinlem  35070  isbasisrelowllem1  35078  isbasisrelowllem2  35079  rdgeqoa  35093  finxpreclem4  35117  finxpsuclem  35120  wl-ifp4impr  35190  wl-1xor  35205  uncf  35342  phpreu  35347  cos2h  35354  tan2h  35355  matunitlindflem1  35359  poimirlem16  35379  poimirlem19  35382  poimirlem23  35386  poimirlem24  35387  poimirlem26  35389  poimirlem27  35390  mbfposadd  35410  cnambfre  35411  itg2addnclem  35414  itg2addnc  35417  iblabsnclem  35426  ftc1anclem1  35436  ftc1anclem5  35440  caures  35504  heiborlem3  35557  heiborlem10  35564  elghomOLD  35631  divrngidl  35772  eqrelf  35983  brvbrvvdif  35991  eldmqsres2  36010  exanres  36018  ssrel3  36022  relcnveq  36045  iss2  36067  ecinn0  36073  brxrn2  36093  ecxrn  36105  eldmcoss2  36165  eldm1cossres  36166  elrelsrel  36193  elrelscnveq  36198  elcoeleqvrelsrel  36297  brredundsredund  36328  brdmqssqs  36348  cnvepresdmqss  36352  eldmqs1cossres  36359  brerser  36376  erim2  36377  eleldisjseldisj  36428  prtlem10  36467  prtlem16  36471  prtlem19  36480  prtex  36482  prter3  36484  islshpat  36619  lcvbr2  36624  lcvbr3  36625  lshpsmreu  36711  isat3  36909  hlrelat5N  37003  islpln5  37137  cdlemblem  37395  paddvaln0N  37403  paddval0  37412  cdlemefrs29bpre1  37999  cdlemefrs29cpre1  38000  cdlemg27b  38298  cdlemg33c  38310  cdlemg33e  38312  diaglbN  38657  cdlemm10N  38720  dicopelval2  38783  dicelval2N  38784  dihopelvalcpre  38850  dihglbcpreN  38902  dih1dimatlem  38931  dihatexv  38940  dvh4dimlem  39045  mapdpglem3  39277  hdmap14lem13  39482  hdmapglem7a  39529  fnsnbt  39743  fsuppind  39812  isnacs2  40048  rabrenfdioph  40156  expdiophlem1  40363  pw2f1ocnv  40379  pwfi2f1o  40441  numinfctb  40448  dfacbasgrp  40453  islnr3  40460  isdomn3  40549  dfhe3  40877  clsk3nimkb  41144  ntrneiiso  41195  ntrneikb  41198  scottabf  41349  mnuunid  41386  hashnzfzclim  41427  dvconstbi  41439  sbcoreleleqVD  41966  rfcnpre3  42063  rfcnpre4  42064  cncfshift  42910  stoweidlem59  43095  dfafv23  44205  nelbrnel  44228  elsetpreimafvrab  44307  iccpartiun  44347  prproropf1olem0  44415  prprelb  44429  prprspr2  44431  reuprpr  44436  oddm1evenALTV  44588  oddp1evenALTV  44589  oddprmne2  44628  fpprel  44641  submgmacs  44819  ismhm0  44820  iscmgmALT  44879  iscsgrpALT  44881  isrnghmmul  44912  iscnrm3  45664  elpglem2  45705