Theorem bitr3id 284

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3id.1	⊢ (𝜓 ↔ 𝜑)
bitr3id.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
bitr3id	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem bitr3id

Step	Hyp	Ref	Expression
1		bitr3id.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 223	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3id.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrid 282	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:  3bitr3g  312  biass  383  imbibi  390  sbcom2  2162  19.16  2213  19.19  2217  necon1bbid  2970  rspc2gv  3617  elabgtOLDOLD  3660  reuxfr1d  3743  sbceq1a  3785  sbcg  3853  sbcralt  3863  sbccsb2  4435  csbie2df  4441  reuprg0  4707  disjxun  5146  dmopab2rex  5919  dfres3  5989  xp11  6179  ressn  6289  fnssresb  6676  dmfco  6991  dffo4  7110  f1ompt  7118  funressn  7166  elunirnALT  7260  fliftf  7320  resoprab2  7537  elrnmpores  7557  ralrnmpo  7558  iunpw  7772  ordunisuc2  7847  tfis  7858  tfinds  7863  dfom2  7871  fiun  7945  f1iun  7946  opiota  8062  1stconst  8103  2ndconst  8104  fnsuppeq0  8195  iinon  8359  dfsmo2  8366  oeeui  8621  omabs  8670  naddrid  8702  brecop  8827  ixpsnf1o  8955  boxcutc  8958  ac6sfi  9310  wemapwe  9720  dmttrcl  9744  sdom2en01  10325  ac6num  10502  zorn2lem7  10525  ttukeylem6  10537  alephval2  10595  fpwwe2  10666  fpwwe  10669  nqereu  10952  suplem2pr  11076  map2psrpr  11133  supsrlem  11134  fimaxre3  12190  infm3  12203  crne0  12235  nn1suc  12264  xmulneg1  13280  supxrbnd1  13332  supxrbnd2  13333  iccneg  13481  wrdmap  14528  wrdind  14704  rtrclreclem3  15039  cnpart  15219  sqrt00  15242  lo1resb  15540  o1resb  15542  absefib  16174  efieq1re  16175  sadadd2lem2  16424  saddisjlem  16438  prmind2  16655  isprm7  16678  mreacs  17637  issubc  17820  isfunc  17849  pospo  18336  mndind  18784  eqgval  19136  resscntz  19288  frgpuplem  19731  qusabl  19824  dmdprd  19959  dprdcntz2  19999  dprd2d2  20005  isnzr2  20461  chrdvds  21460  chrcong  21461  znleval  21492  isphld  21590  mpfind  22060  gsummoncoe1  22236  pf1ind  22283  smadiadetr  22607  mp2pm2mplem4  22741  isclo  23021  ist1-2  23281  isnrm2  23292  bwth  23344  nconnsubb  23357  subislly  23415  ptclsg  23549  qtopcld  23647  kqcldsat  23667  qustgplem  24055  tsmssubm  24077  ustuqtop  24181  utop2nei  24185  blval2  24501  caucfil  25241  ioorinv  25535  mbfss  25605  iblss2  25765  dvivthlem1  25971  lhop1  25977  deg1leb  26061  reeff1o  26414  sincosq3sgn  26465  sincosq4sgn  26466  dcubic  26808  efrlim  26931  efrlimOLD  26932  fsumharmonic  26974  isppw  27076  issqf  27098  fsumdvdsmul  27157  fsumdvdsmulOLD  27159  ppiub  27167  lgsdinn0  27308  noetainflem4  27703  eqscut  27768  mulsprop  28064  tglngne  28410  tgelrnln  28490  axlowdimlem14  28822  nbgrssovtx  29230  clwwlknclwwlkdif  29845  eupth2lem2  30085  fusgr2wsp2nb  30200  h2hlm  30846  isch2  31089  ch0pss  31311  nmcfnlbi  31918  jplem1  32134  hatomistici  32228  mdsymlem5  32273  cdjreui  32298  dfimafnf  32478  funcnvmpt  32510  fpwrelmap  32572  nn0min  32640  wrdt2ind  32731  swrdrn3  32733  isarchi  32947  zarcls  33545  ordtconnlem1  33595  esumfsup  33759  esumpcvgval  33767  measvuni  33903  aean  33933  eulerpartlemgh  34068  ballotlemsima  34205  sgn3da  34231  bnj1468  34547  subfacp1lem2a  34860  subfacp1lem6  34865  goeleq12bg  35029  dmopab3rexdif  35085  eldm3  35425  onsuct0  35995  bj-equsexvwd  36328  currysetlem1  36496  bj-restsn  36631  ptrest  37162  ptrecube  37163  poimirlem2  37165  poimirlem23  37186  sdclem2  37285  fdc  37288  fdc1  37289  istotbnd3  37314  sstotbnd  37318  prdstotbnd  37337  rrncmslem  37375  brinxprnres  37832  brcnvrabga  37883  alrmomodm  37900  br1cossxrnres  37989  lub0N  38730  glb0N  38734  cdlemefrs29bpre0  39938  dvhb1dimN  40528  dvhopellsm  40659  dibord  40701  dochnel2  40934  mapdvalc  41171  mapdval4N  41174  diophin  42257  diophun  42258  diophrex  42260  3rexfrabdioph  42282  6rexfrabdioph  42284  7rexfrabdioph  42285  zindbi  42432  tfsconcatrn  42836  rababg  43069  relexpnul  43173  clsk1independent  43541  scottabf  43742  hashnzfzclim  43824  fveqsb  43955  infxrbnd2  44814  cncfiooicclem1  45344  stoweidlem35  45486  tz6.12-afv  46616  ndmaovg  46627  tz6.12-afv2  46683  ich2exprop  46874  prprspr2  46921  line2x  47939  line2y  47940  itsclc0b  47957  clddisj  48034  aacllem  48346