Theorem bitr4di 288

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3bitr4g  313  bibi2i  337  mtt  364  nbn2  370  ifptru  1072  3bior1fd  1473  3biant1d  1476  clelabOLD  2883  clel4g  3586  eueq3  3641  sbceqal  3778  n0moeu  4287  sbcel12  4339  sbceqg  4340  sbcne12  4343  reldisj  4382  reldisjOLD  4383  raldifeq  4421  r19.3rz  4424  ralf0  4441  eldifpr  4590  reusngf  4605  rexreusng  4612  eldiftp  4619  reusv2lem5  5320  prelpw  5356  otthg  5394  2rbropap  5470  rabxp  5626  pwvrel  5628  elrng  5789  iss  5932  idrefALT  6007  xpcan  6068  xpcan2  6069  dfpo2  6188  ordelpss  6279  fcnvres  6635  dffv3  6752  funimass4  6816  unima  6825  fndmdif  6901  fneqeql  6905  funimass3  6913  elrnrexdmb  6948  dff4  6959  fnsnb  7020  fconst4  7072  elunirn  7106  f12dfv  7126  riota1  7234  riota2df  7236  f1ocnvfv3  7251  eqfnov  7381  elrnmpores  7389  caoftrn  7549  ordsucun  7647  dflim3  7669  dfom2  7689  peano5  7714  peano5OLD  7715  opiota  7872  suppssr  7983  mpoxopovel  8007  brtpos  8022  rntpos  8026  ordgt0ge1  8289  ondif2  8294  oelim2  8388  omabs  8441  iiner  8536  erinxp  8538  qliftfun  8549  mapdm0  8588  ordunifi  8994  elfi2  9103  elfiun  9119  fifo  9121  noinfep  9348  cantnflem1  9377  cantnf  9381  rankonidlem  9517  r1pwALT  9535  pr2nelem  9691  cardalephex  9777  alephinit  9782  dfac5lem4  9813  cflim2  9950  cfsmolem  9957  compssiso  10061  fin1a2lem11  10097  itunisuc  10106  axdclem  10206  brdom6disj  10219  alephreg  10269  fpwwe2lem8  10325  pwfseqlem3  10347  pwfseqlem4  10349  indpi  10594  nqereu  10616  ordpinq  10630  ltanq  10658  ltmnq  10659  suplem2pr  10740  map2psrpr  10797  ssxr  10975  leltne  10995  ltneg  11405  leneg  11408  suprnub  11870  negiso  11885  elnnnn0  12206  nn0sub  12213  frnnn0fsupp  12220  zrevaddcl  12295  znnsub  12296  znn0sub  12297  prime  12331  eluz2  12517  indstr  12585  eluz2b1  12588  qrevaddcl  12640  rpneg  12691  xrleltne  12808  dfle2  12810  dflt2  12811  supxrleub  12989  infxrgelb  12998  ixxin  13025  iccid  13053  elicopnf  13106  iccsplit  13146  fzsplit2  13210  fzsn  13227  fzpr  13240  uzsplit  13257  preduz  13307  fvinim0ffz  13434  injresinj  13436  om2uzf1oi  13601  lt2sqi  13834  le2sqi  13835  hashsdom  14024  hashf1lem1  14096  hashf1lem1OLD  14097  fz1isolem  14103  prprrab  14115  ccatlcan  14359  ccatrcan  14360  s3eq3seq  14580  2swrd2eqwrdeq  14594  trclfvcotr  14648  cnpart  14879  limsuplt  15116  rlimresb  15202  mertenslem2  15525  fprod2dlem  15618  sadadd2lem2  16085  saddisjlem  16099  bitsuz  16109  gcddiv  16187  algcvgblem  16210  isprm3  16316  isprm5  16340  prmreclem5  16549  vdwapun  16603  vdwmc2  16608  ramcl  16658  pwsle  17120  ismre  17216  mreacs  17284  acsfn  17285  iscatd2  17307  cidpropd  17336  dfiso2  17401  oppcsect2  17408  isfunc  17495  setcinv  17721  lubeldm  17986  lubval  17989  glbeldm  17999  glbval  18002  tosso  18052  ipodrsfi  18172  acsfiindd  18186  imasmnd2  18337  resmndismnd  18362  submacs  18380  imasgrp2  18605  issubg  18670  resgrpisgrp  18691  subgacs  18704  eqgval  18720  gaorber  18829  symgfix2  18939  psgnran  19038  isslw  19128  sylow2alem2  19138  sylow2a  19139  sylow3lem6  19152  efgcpbllemb  19276  prmcyg  19410  gsum2d2lem  19489  gsumcom2  19491  subgdmdprd  19552  dprd2d2  19562  pgpfac1lem2  19593  pgpfac1lem4  19596  imasring  19773  drngmulne0  19928  subrgacs  19983  sdrgacs  19984  lssle0  20126  lssacs  20144  lssats2  20177  lvecvsn0  20286  islpir  20433  isnzr2  20447  zndvds  20669  znleval  20674  znleval2  20675  lindsmm  20945  islinds3  20951  islindf4  20955  ismhp3  21243  eltg2b  22017  discld  22148  opnssneib  22174  cldlp  22209  restbas  22217  leordtvallem1  22269  leordtvallem2  22270  ssidcn  22314  cnprest2  22349  lmss  22357  perfcls  22424  cmpfi  22467  1stccnp  22521  subislly  22540  hausmapdom  22559  locfindis  22589  iskgen3  22608  kgencn  22615  ptpjpre1  22630  xkoccn  22678  txrest  22690  txlm  22707  txkgen  22711  xkopt  22714  xkoinjcn  22746  imasnopn  22749  imasncld  22750  imasncls  22751  qtopcn  22773  kqfeq  22783  isr0  22796  fbfinnfr  22900  trfbas  22903  fbunfip  22928  ufileu  22978  cfinufil  22987  fmid  23019  txflf  23065  fclsrest  23083  alexsubALT  23110  tsmsres  23203  ucnima  23341  fmucndlem  23351  bldisj  23459  xmeter  23494  elbl4  23625  restmetu  23632  dscopn  23635  bl2ioo  23861  isphtpc  24063  tcphcph  24306  lmmbr2  24328  lmmbrf  24331  iscau2  24346  iscauf  24349  caucfil  24352  metcld  24375  metcld2  24376  bcthlem1  24393  bcthlem4  24396  cldcss2  24511  ovolgelb  24549  ovoliunlem1  24571  ismbfcn  24698  mbfmax  24718  mbfimaopnlem  24724  i1faddlem  24762  i1fmullem  24763  i1fres  24775  i1fpos  24776  itg1climres  24784  xrge0f  24801  itgresr  24848  iblcnlem1  24857  limcun  24964  dvres  24980  mdegmullem  25148  ply1remlem  25232  plyremlem  25369  vieta1  25377  ulmcau  25459  sineq0  25585  coseq1  25586  ang180lem3  25866  cubic  25904  atandm  25931  atandm2  25932  atandm3  25933  rlimcnp  26020  rlimcnp2  26021  vmappw  26170  dchrelbas3  26291  dchrelbas4  26296  dchrsum2  26321  bposlem6  26342  2sqreuopltb  26518  2sqreuopnnltb  26520  dchrisumlem3  26544  pntleml  26664  istrkg3ld  26726  tgcgr4  26796  lnrot2  26889  islnopp  27004  islmib  27052  brbtwn2  27176  axsegconlem6  27193  axsegcon  27198  ax5seg  27209  axpasch  27212  axeuclid  27234  axcontlem4  27238  elntg2  27256  issubgr  27541  nb3gr2nb  27654  uhgrvd00  27804  isrusgr0  27836  wlkcpr  27898  wlkcomp  27900  upgr2wlk  27938  upgrf1istrl  27973  clwlkcomp  28048  clwlkcompbp  28051  iswwlksnx  28106  wspthsnwspthsnon  28182  wspniunwspnon  28189  2pthon3v  28209  usgr2wspthons3  28230  usgr2wspthon  28231  rusgrnumwwlks  28240  clwlkclwwlklem3  28266  clwlkclwwlk  28267  clwwlknonwwlknonb  28371  0pth  28390  eupth2lem2  28484  vdgn1frgrv2  28561  fusgreg2wsp  28601  clwwlknonclwlknonf1o  28627  dlwwlknondlwlknonf1o  28630  wlkl0  28632  nmoolb  29034  nmlno0lem  29056  ubthlem1  29133  ocsh  29546  shle0  29705  eigrei  30097  adjeu  30152  nmoplb  30170  nmfnlb  30187  eleigvec2  30221  nmlnop0iALT  30258  cnlnadjlem5  30334  adjbdln  30346  jplem2  30532  cvbr2  30546  mdsl2bi  30586  chrelat3  30634  sq2reunnltb  30734  rmounid  30744  eqrrabd  30750  eqsnd  30778  nelpr  30780  disjunsn  30834  ofpreima  30904  funcnvmpt  30906  funcnv5mpt  30907  dfcnv2  30915  suppiniseg  30922  gtiso  30935  fpwrelmap  30970  infxrge0glb  30990  xrdifh  31003  fzsplit3  31017  swrdrn3  31129  toslublem  31152  tosglblem  31154  mgcval  31167  xrge0tsmsbi  31220  cntzun  31222  isarchi  31338  lsmsnorb  31481  nsgqusf1olem2  31501  isprmidl  31515  smatrcl  31648  ist0cld  31685  rspectopn  31719  zarcls  31726  rhmpreimacnlem  31736  unitdivcld  31753  lmxrge0  31804  isrrext  31850  issibf  32200  eulerpartlemr  32241  eulerpartlemmf  32242  eulerpartlemn  32248  dstfrvunirn  32341  ballotlemfc0  32359  ballotlemfcc  32360  reprsuc  32495  reprpmtf1o  32506  reprdifc  32507  bnj919  32647  bnj976  32657  bnj1542  32737  bnj150  32756  bnj151  32757  bnj607  32796  bnj852  32801  bnj873  32804  bnj938  32817  bnj1171  32880  bnj1388  32913  bnj1489  32936  nummin  32963  usgrgt2cycl  32992  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem9  33061  kur14  33078  iscvm  33121  satf0op  33239  mclsax  33431  elintfv  33644  fundmpss  33646  opelco3  33655  dfon2  33674  frxp2  33718  xpord2pred  33719  xpord2ind  33721  xpord3ind  33727  naddid1  33763  noetasuplem4  33866  noetainflem4  33870  addsid1  34054  dfbigcup2  34128  sscoid  34142  funpartfv  34174  dfrdg4  34180  cgr3permute3  34276  segletr  34343  segleantisym  34344  seglelin  34345  fneval  34468  neibastop3  34478  eltail  34490  filnetlem4  34497  bj-hbntbi  34813  bj-equsvt  34888  bj-sbceqgALT  35014  bj-clel3gALT  35148  bj-rest10  35186  bj-0int  35199  topdifinffinlem  35445  isbasisrelowllem1  35453  isbasisrelowllem2  35454  rdgeqoa  35468  finxpreclem4  35492  finxpsuclem  35495  wl-ifp4impr  35565  wl-1xor  35580  uncf  35683  phpreu  35688  cos2h  35695  tan2h  35696  matunitlindflem1  35700  poimirlem16  35720  poimirlem19  35723  poimirlem23  35727  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  mbfposadd  35751  cnambfre  35752  itg2addnclem  35755  itg2addnc  35758  iblabsnclem  35767  ftc1anclem1  35777  ftc1anclem5  35781  caures  35845  heiborlem3  35898  heiborlem10  35905  elghomOLD  35972  divrngidl  36113  eqrelf  36322  brvbrvvdif  36330  eldmqsres2  36349  exanres  36357  ssrel3  36361  relcnveq  36384  iss2  36406  ecinn0  36412  brxrn2  36432  ecxrn  36444  eldmcoss2  36504  eldm1cossres  36505  elrelsrel  36532  elrelscnveq  36537  elcoeleqvrelsrel  36636  brredundsredund  36667  brdmqssqs  36687  cnvepresdmqss  36691  eldmqs1cossres  36698  brerser  36715  erim2  36716  eleldisjseldisj  36767  prtlem10  36806  prtlem16  36810  prtlem19  36819  prtex  36821  prter3  36823  islshpat  36958  lcvbr2  36963  lcvbr3  36964  lshpsmreu  37050  isat3  37248  hlrelat5N  37342  islpln5  37476  cdlemblem  37734  paddvaln0N  37742  paddval0  37751  cdlemefrs29bpre1  38338  cdlemefrs29cpre1  38339  cdlemg27b  38637  cdlemg33c  38649  cdlemg33e  38651  diaglbN  38996  cdlemm10N  39059  dicopelval2  39122  dicelval2N  39123  dihopelvalcpre  39189  dihglbcpreN  39241  dih1dimatlem  39270  dihatexv  39279  dvh4dimlem  39384  mapdpglem3  39616  hdmap14lem13  39821  hdmapglem7a  39868  fnsnbt  40134  fsuppind  40202  isnacs2  40444  rabrenfdioph  40552  expdiophlem1  40759  pw2f1ocnv  40775  pwfi2f1o  40837  numinfctb  40844  dfacbasgrp  40849  islnr3  40856  isdomn3  40945  dfhe3  41272  clsk3nimkb  41539  ntrneiiso  41590  ntrneikb  41593  scottabf  41747  mnuunid  41784  hashnzfzclim  41829  dvconstbi  41841  sbcoreleleqVD  42368  rfcnpre3  42465  rfcnpre4  42466  cncfshift  43305  stoweidlem59  43490  dfafv23  44632  nelbrnel  44655  elsetpreimafvrab  44734  iccpartiun  44774  prproropf1olem0  44842  prprelb  44856  prprspr2  44858  reuprpr  44863  oddm1evenALTV  45015  oddp1evenALTV  45016  oddprmne2  45055  fpprel  45068  submgmacs  45246  ismhm0  45247  iscmgmALT  45306  iscsgrpALT  45308  isrnghmmul  45339  mofeu  46063  iscnrm3  46134  joindm2  46150  meetdm2  46152  elpglem2  46303