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  912  dn1dc  969  bilukdc  1441  nf4dc  1718  sbal1  2058  abbibcom  2348  abbib  2352  necon3abid  2453  necon3bid  2455  necon1abiidc  2474  r19.21t  2619  ceqsralt  2843  ceqsrexv  2949  ceqsrex2v  2951  elab2g  2966  elrabf  2973  eueq2dc  2992  euxfrdc  3005  eqreu  3011  reu8  3015  ru  3043  sbcralt  3121  sbcrext  3122  sbcne12g  3158  csbnestgf  3193  dfss4st  3456  rexsng  3732  ralprg  3742  rexprg  3743  difsn  3833  opthpr  3878  ralunsn  3904  dfiin2g  4026  iunxsng  4069  iunxsngf  4071  elpwuni  4083  pwnss  4274  exmid01  4313  opelopabt  4382  opelopabga  4383  brabga  4384  opelopabgf  4390  elsucg  4527  elsuc2g  4528  brab2a  4805  opeliunxp  4807  posng  4824  brab2ga  4827  csbdmg  4952  elrnmpt1  5010  elrnmptg  5011  eliniseg2  5144  poleloe  5164  elxp4  5252  elxp5  5253  cnvpom  5307  sbcfung  5378  dffun8  5382  fncnv  5424  fununi  5426  fnssresb  5472  fnimaeq0  5482  funcocnv2  5641  dffn5im  5724  funimass4  5729  fnsnfv  5738  dmfco  5747  fndmdif  5785  fndmin  5787  unpreima  5804  respreima  5807  fsn2  5853  fnressn  5872  fressnfv  5873  elunirn  5941  dff13  5943  fliftel  5968  isoini  5993  f1oiso  6001  riotaeqimp  6030  acexmid  6051  fnbrovb  6097  eloprabga  6142  resoprab2  6152  ralrnmpo  6170  rexrnmpo  6171  ovid  6172  ov  6175  ovg  6195  ofrfval2  6285  fmpox  6398  1stconst  6419  2ndconst  6420  f1od2  6433  rbropapd  6475  brtpos2  6484  dfsmo2  6520  frecabcl  6632  brdifun  6796  eqerlem  6800  brecop  6861  erovlem  6863  mapsnd  6925  mapsn  6927  mptelixpg  6971  map1  7056  xpsnen  7074  xpdom2  7084  xpf1o  7099  mapunen  7106  supubti  7292  infglbti  7318  ctssdccl  7404  nninfwlpoim  7472  nninfinfwlpo  7473  netap  7573  2omotaplemap  7576  ltpiord  7639  nlt1pig  7661  elinp  7794  ltdfpr  7826  genpassl  7844  genpassu  7845  1idprl  7910  1idpru  7911  gt0srpr  8068  mappsrprg  8124  map2psrprg  8125  peano2nnnn  8173  recidpirq  8178  axprecex  8200  xrlenlt  8343  addsubeq4  8493  renegcl  8539  lesub0  8758  recexaplem2  8931  conjmulap  9008  rerecclap  9009  creui  9239  peano2nn  9254  nndiv  9283  elznn0  9597  eqreznegel  9952  negelrp  10026  ltxr  10114  divelunit  10341  iccf1o  10344  elfz2  10355  elfzp1  10413  fzdifsuc  10422  fznn  10430  nelfzo  10493  fzosplitsni  10588  fvinim0ffz  10594  infssuzex  10600  zsupssdc  10605  frec2uzisod  10776  sq11i  10998  wrdval  11235  csbwrdg  11262  swrdnd  11359  wrd2ind  11423  cjreb  11559  rexfiuz  11682  cau3lem  11807  pwm1geoserap1  12202  mertensabs  12231  divides  12483  dvdsabseq  12541  odd2np1  12567  oddm1even  12569  modremain  12623  bezoutlemnewy  12700  bezoutlemstep  12701  bezoutlemmain  12702  bezoutlema  12703  bezoutlemb  12704  isprm2  12822  isprm4  12824  dvdsnprmd  12830  oddprmdvds  13060  4sqlem2  13095  4sqlem12  13108  xpsfrnel2  13580  issubm  13706  grplmulf1o  13808  grplactcnv  13836  issubg  13911  elnmz  13946  isghm  13981  ghmeqker  14009  srg1zr  14152  iscrng2  14180  issubrng  14367  aprval  14451  zndvds  14846  znleval  14850  psrbag  14866  istopg  14913  basgen2  14995  isnei  15058  restdis  15098  iscn  15111  iscnp  15113  lmbr2  15128  lmbrf  15129  txcn  15189  cnmpt21  15205  blres  15348  isxms2  15366  metrest  15420  metcnp  15426  txmetcnp  15432  txmetcn  15433  cnblcld  15449  reopnap  15460  ioocosf1o  15768  mpodvdsmulf1o  15907  gausslemma2dlem0i  15979  gausslemma2dlem1a  15980  lgseisenlem2  15993  lgsquadlem1  15999  lgsquadlem2  16000  2lgslem1a  16010  isuhgrm  16115  isushgrm  16116  isupgren  16139  isumgren  16149  isuspgren  16201  isusgren  16202  uhgr0v0e  16278  vtxdg0v  16338  iswlk  16367  wlk1walkdom  16403  istrl  16429  clwwlkn1  16462  clwwlkn2  16465  clwwlknonel  16476  clwwlknun  16485  iseupth  16491  eupthres  16501  eupth2lem1  16502  eupth2lemsfi  16522  bj-nn0sucALT  16797  apdiff  16881