Theorem bitrid 192

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

Hypotheses

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

Assertion

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

Proof of Theorem bitrid

Step	Hyp	Ref	Expression
1		bitrid.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3		bitrid.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 188	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2id  193  bitr3id  194  3bitr4g  223  imim21b  253  pm5.17dc  905  dn1dc  962  bilukdc  1407  nf4dc  1681  sbal1  2018  abbi  2307  necon3abid  2403  necon3bid  2405  necon1abiidc  2424  r19.21t  2569  ceqsralt  2787  ceqsrexv  2890  ceqsrex2v  2892  elab2g  2907  elrabf  2914  eueq2dc  2933  euxfrdc  2946  eqreu  2952  reu8  2956  ru  2984  sbcralt  3062  sbcrext  3063  sbcne12g  3098  csbnestgf  3133  dfss4st  3392  rexsng  3659  ralprg  3669  rexprg  3670  difsn  3755  opthpr  3798  ralunsn  3823  dfiin2g  3945  iunxsng  3988  iunxsngf  3990  elpwuni  4002  pwnss  4188  exmid01  4227  opelopabt  4292  opelopabga  4293  brabga  4294  opelopabgf  4300  elsucg  4435  elsuc2g  4436  brab2a  4712  opeliunxp  4714  posng  4731  brab2ga  4734  csbdmg  4856  elrnmpt1  4913  elrnmptg  4914  eliniseg2  5045  poleloe  5065  elxp4  5153  elxp5  5154  cnvpom  5208  sbcfung  5278  dffun8  5282  fncnv  5320  fununi  5322  fnssresb  5366  fnimaeq0  5375  funcocnv2  5525  dffn5im  5602  funimass4  5607  fnsnfv  5616  dmfco  5625  fndmdif  5663  fndmin  5665  unpreima  5683  respreima  5686  fsn2  5732  fnressn  5744  fressnfv  5745  elunirn  5809  dff13  5811  fliftel  5836  isoini  5861  f1oiso  5869  acexmid  5917  eloprabga  6005  resoprab2  6015  ralrnmpo  6033  rexrnmpo  6034  ovid  6035  ov  6038  ovg  6057  ofrfval2  6147  fmpox  6253  1stconst  6274  2ndconst  6275  f1od2  6288  rbropapd  6295  brtpos2  6304  dfsmo2  6340  frecabcl  6452  brdifun  6614  eqerlem  6618  brecop  6679  erovlem  6681  mapsn  6744  mptelixpg  6788  map1  6866  xpsnen  6875  xpdom2  6885  xpf1o  6900  supubti  7058  infglbti  7084  ctssdccl  7170  nninfwlpoim  7237  netap  7314  2omotaplemap  7317  ltpiord  7379  nlt1pig  7401  elinp  7534  ltdfpr  7566  genpassl  7584  genpassu  7585  1idprl  7650  1idpru  7651  gt0srpr  7808  mappsrprg  7864  map2psrprg  7865  peano2nnnn  7913  recidpirq  7918  axprecex  7940  xrlenlt  8084  addsubeq4  8234  renegcl  8280  lesub0  8498  recexaplem2  8671  conjmulap  8748  rerecclap  8749  creui  8979  peano2nn  8994  nndiv  9023  elznn0  9332  eqreznegel  9679  negelrp  9753  ltxr  9841  divelunit  10068  iccf1o  10070  elfz2  10081  elfzp1  10138  fzdifsuc  10147  fznn  10155  nelfzo  10218  fzosplitsni  10302  fvinim0ffz  10308  frec2uzisod  10478  sq11i  10700  wrdval  10917  csbwrdg  10943  cjreb  11010  rexfiuz  11133  cau3lem  11258  pwm1geoserap1  11651  mertensabs  11680  divides  11932  dvdsabseq  11989  odd2np1  12014  oddm1even  12016  modremain  12070  infssuzex  12086  zsupssdc  12091  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlema  12136  bezoutlemb  12137  isprm2  12255  isprm4  12257  dvdsnprmd  12263  oddprmdvds  12492  4sqlem2  12527  4sqlem12  12540  xpsfrnel2  12929  issubm  13044  grplmulf1o  13146  grplactcnv  13174  issubg  13243  elnmz  13278  isghm  13313  ghmeqker  13341  srg1zr  13483  iscrng2  13511  issubrng  13695  aprval  13778  zndvds  14137  znleval  14141  psrbag  14155  istopg  14167  basgen2  14249  isnei  14312  restdis  14352  iscn  14365  iscnp  14367  lmbr2  14382  lmbrf  14383  txcn  14443  cnmpt21  14459  blres  14602  isxms2  14620  metrest  14674  metcnp  14680  txmetcnp  14686  txmetcn  14687  cnblcld  14703  reopnap  14706  ioocosf1o  14989  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  lgseisenlem2  15187  lgsquadlem1  15191  bj-nn0sucALT  15470  apdiff  15538