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  906  dn1dc  963  bilukdc  1416  nf4dc  1694  sbal1  2031  abbi  2321  necon3abid  2417  necon3bid  2419  necon1abiidc  2438  r19.21t  2583  ceqsralt  2804  ceqsrexv  2910  ceqsrex2v  2912  elab2g  2927  elrabf  2934  eueq2dc  2953  euxfrdc  2966  eqreu  2972  reu8  2976  ru  3004  sbcralt  3082  sbcrext  3083  sbcne12g  3119  csbnestgf  3154  dfss4st  3414  rexsng  3684  ralprg  3694  rexprg  3695  difsn  3781  opthpr  3826  ralunsn  3852  dfiin2g  3974  iunxsng  4017  iunxsngf  4019  elpwuni  4031  pwnss  4219  exmid01  4258  opelopabt  4326  opelopabga  4327  brabga  4328  opelopabgf  4334  elsucg  4469  elsuc2g  4470  brab2a  4746  opeliunxp  4748  posng  4765  brab2ga  4768  csbdmg  4891  elrnmpt1  4948  elrnmptg  4949  eliniseg2  5081  poleloe  5101  elxp4  5189  elxp5  5190  cnvpom  5244  sbcfung  5314  dffun8  5318  fncnv  5359  fununi  5361  fnssresb  5407  fnimaeq0  5417  funcocnv2  5569  dffn5im  5647  funimass4  5652  fnsnfv  5661  dmfco  5670  fndmdif  5708  fndmin  5710  unpreima  5728  respreima  5731  fsn2  5777  fnressn  5793  fressnfv  5794  elunirn  5858  dff13  5860  fliftel  5885  isoini  5910  f1oiso  5918  acexmid  5966  eloprabga  6055  resoprab2  6065  ralrnmpo  6083  rexrnmpo  6084  ovid  6085  ov  6088  ovg  6108  ofrfval2  6198  fmpox  6309  1stconst  6330  2ndconst  6331  f1od2  6344  rbropapd  6351  brtpos2  6360  dfsmo2  6396  frecabcl  6508  brdifun  6670  eqerlem  6674  brecop  6735  erovlem  6737  mapsn  6800  mptelixpg  6844  map1  6928  xpsnen  6941  xpdom2  6951  xpf1o  6966  supubti  7127  infglbti  7153  ctssdccl  7239  nninfwlpoim  7307  nninfinfwlpo  7308  netap  7401  2omotaplemap  7404  ltpiord  7467  nlt1pig  7489  elinp  7622  ltdfpr  7654  genpassl  7672  genpassu  7673  1idprl  7738  1idpru  7739  gt0srpr  7896  mappsrprg  7952  map2psrprg  7953  peano2nnnn  8001  recidpirq  8006  axprecex  8028  xrlenlt  8172  addsubeq4  8322  renegcl  8368  lesub0  8587  recexaplem2  8760  conjmulap  8837  rerecclap  8838  creui  9068  peano2nn  9083  nndiv  9112  elznn0  9422  eqreznegel  9770  negelrp  9844  ltxr  9932  divelunit  10159  iccf1o  10161  elfz2  10172  elfzp1  10229  fzdifsuc  10238  fznn  10246  nelfzo  10309  fzosplitsni  10401  fvinim0ffz  10407  infssuzex  10413  zsupssdc  10418  frec2uzisod  10589  sq11i  10811  wrdval  11034  csbwrdg  11060  swrdnd  11150  wrd2ind  11214  cjreb  11292  rexfiuz  11415  cau3lem  11540  pwm1geoserap1  11934  mertensabs  11963  divides  12215  dvdsabseq  12273  odd2np1  12299  oddm1even  12301  modremain  12355  bezoutlemnewy  12432  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlema  12435  bezoutlemb  12436  isprm2  12554  isprm4  12556  dvdsnprmd  12562  oddprmdvds  12792  4sqlem2  12827  4sqlem12  12840  xpsfrnel2  13293  issubm  13419  grplmulf1o  13521  grplactcnv  13549  issubg  13624  elnmz  13659  isghm  13694  ghmeqker  13722  srg1zr  13864  iscrng2  13892  issubrng  14076  aprval  14159  zndvds  14526  znleval  14530  psrbag  14546  istopg  14586  basgen2  14668  isnei  14731  restdis  14771  iscn  14784  iscnp  14786  lmbr2  14801  lmbrf  14802  txcn  14862  cnmpt21  14878  blres  15021  isxms2  15039  metrest  15093  metcnp  15099  txmetcnp  15105  txmetcn  15106  cnblcld  15122  reopnap  15133  ioocosf1o  15441  mpodvdsmulf1o  15577  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  2lgslem1a  15680  isuhgrm  15782  isushgrm  15783  isupgren  15806  isumgren  15816  bj-nn0sucALT  16113  apdiff  16189