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  909  dn1dc  966  bilukdc  1438  nf4dc  1716  sbal1  2053  abbi  2343  necon3abid  2439  necon3bid  2441  necon1abiidc  2460  r19.21t  2605  ceqsralt  2828  ceqsrexv  2934  ceqsrex2v  2936  elab2g  2951  elrabf  2958  eueq2dc  2977  euxfrdc  2990  eqreu  2996  reu8  3000  ru  3028  sbcralt  3106  sbcrext  3107  sbcne12g  3143  csbnestgf  3178  dfss4st  3438  rexsng  3708  ralprg  3718  rexprg  3719  difsn  3808  opthpr  3853  ralunsn  3879  dfiin2g  4001  iunxsng  4044  iunxsngf  4046  elpwuni  4058  pwnss  4247  exmid01  4286  opelopabt  4354  opelopabga  4355  brabga  4356  opelopabgf  4362  elsucg  4499  elsuc2g  4500  brab2a  4777  opeliunxp  4779  posng  4796  brab2ga  4799  csbdmg  4923  elrnmpt1  4981  elrnmptg  4982  eliniseg2  5114  poleloe  5134  elxp4  5222  elxp5  5223  cnvpom  5277  sbcfung  5348  dffun8  5352  fncnv  5393  fununi  5395  fnssresb  5441  fnimaeq0  5451  funcocnv2  5605  dffn5im  5687  funimass4  5692  fnsnfv  5701  dmfco  5710  fndmdif  5748  fndmin  5750  unpreima  5768  respreima  5771  fsn2  5817  fnressn  5835  fressnfv  5836  elunirn  5902  dff13  5904  fliftel  5929  isoini  5954  f1oiso  5962  riotaeqimp  5991  acexmid  6012  fnbrovb  6058  eloprabga  6103  resoprab2  6113  ralrnmpo  6131  rexrnmpo  6132  ovid  6133  ov  6136  ovg  6156  ofrfval2  6247  fmpox  6360  1stconst  6381  2ndconst  6382  f1od2  6395  rbropapd  6403  brtpos2  6412  dfsmo2  6448  frecabcl  6560  brdifun  6724  eqerlem  6728  brecop  6789  erovlem  6791  mapsn  6854  mptelixpg  6898  map1  6982  xpsnen  7000  xpdom2  7010  xpf1o  7025  supubti  7192  infglbti  7218  ctssdccl  7304  nninfwlpoim  7372  nninfinfwlpo  7373  netap  7466  2omotaplemap  7469  ltpiord  7532  nlt1pig  7554  elinp  7687  ltdfpr  7719  genpassl  7737  genpassu  7738  1idprl  7803  1idpru  7804  gt0srpr  7961  mappsrprg  8017  map2psrprg  8018  peano2nnnn  8066  recidpirq  8071  axprecex  8093  xrlenlt  8237  addsubeq4  8387  renegcl  8433  lesub0  8652  recexaplem2  8825  conjmulap  8902  rerecclap  8903  creui  9133  peano2nn  9148  nndiv  9177  elznn0  9487  eqreznegel  9841  negelrp  9915  ltxr  10003  divelunit  10230  iccf1o  10232  elfz2  10243  elfzp1  10300  fzdifsuc  10309  fznn  10317  nelfzo  10380  fzosplitsni  10474  fvinim0ffz  10480  infssuzex  10486  zsupssdc  10491  frec2uzisod  10662  sq11i  10884  wrdval  11109  csbwrdg  11136  swrdnd  11233  wrd2ind  11297  cjreb  11420  rexfiuz  11543  cau3lem  11668  pwm1geoserap1  12062  mertensabs  12091  divides  12343  dvdsabseq  12401  odd2np1  12427  oddm1even  12429  modremain  12483  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlemmain  12562  bezoutlema  12563  bezoutlemb  12564  isprm2  12682  isprm4  12684  dvdsnprmd  12690  oddprmdvds  12920  4sqlem2  12955  4sqlem12  12968  xpsfrnel2  13422  issubm  13548  grplmulf1o  13650  grplactcnv  13678  issubg  13753  elnmz  13788  isghm  13823  ghmeqker  13851  srg1zr  13993  iscrng2  14021  issubrng  14206  aprval  14289  zndvds  14656  znleval  14660  psrbag  14676  istopg  14716  basgen2  14798  isnei  14861  restdis  14901  iscn  14914  iscnp  14916  lmbr2  14931  lmbrf  14932  txcn  14992  cnmpt21  15008  blres  15151  isxms2  15169  metrest  15223  metcnp  15229  txmetcnp  15235  txmetcn  15236  cnblcld  15252  reopnap  15263  ioocosf1o  15571  mpodvdsmulf1o  15707  gausslemma2dlem0i  15779  gausslemma2dlem1a  15780  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  2lgslem1a  15810  isuhgrm  15915  isushgrm  15916  isupgren  15939  isumgren  15949  isuspgren  16001  isusgren  16002  uhgr0v0e  16078  vtxdg0v  16105  iswlk  16134  wlk1walkdom  16170  istrl  16194  clwwlkn1  16227  clwwlkn2  16230  clwwlknonel  16241  clwwlknun  16250  iseupth  16256  eupthres  16266  bj-nn0sucALT  16523  apdiff  16602