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  911  dn1dc  968  bilukdc  1440  nf4dc  1717  sbal1  2054  abbi  2344  necon3abid  2440  necon3bid  2442  necon1abiidc  2461  r19.21t  2606  ceqsralt  2829  ceqsrexv  2935  ceqsrex2v  2937  elab2g  2952  elrabf  2959  eueq2dc  2978  euxfrdc  2991  eqreu  2997  reu8  3001  ru  3029  sbcralt  3107  sbcrext  3108  sbcne12g  3144  csbnestgf  3179  dfss4st  3439  rexsng  3711  ralprg  3721  rexprg  3722  difsn  3811  opthpr  3856  ralunsn  3882  dfiin2g  4004  iunxsng  4047  iunxsngf  4049  elpwuni  4061  pwnss  4251  exmid01  4290  opelopabt  4358  opelopabga  4359  brabga  4360  opelopabgf  4366  elsucg  4503  elsuc2g  4504  brab2a  4781  opeliunxp  4783  posng  4800  brab2ga  4803  csbdmg  4927  elrnmpt1  4985  elrnmptg  4986  eliniseg2  5118  poleloe  5138  elxp4  5226  elxp5  5227  cnvpom  5281  sbcfung  5352  dffun8  5356  fncnv  5398  fununi  5400  fnssresb  5446  fnimaeq0  5456  funcocnv2  5611  dffn5im  5694  funimass4  5699  fnsnfv  5708  dmfco  5717  fndmdif  5755  fndmin  5757  unpreima  5775  respreima  5778  fsn2  5824  fnressn  5843  fressnfv  5844  elunirn  5912  dff13  5914  fliftel  5939  isoini  5964  f1oiso  5972  riotaeqimp  6001  acexmid  6022  fnbrovb  6068  eloprabga  6113  resoprab2  6123  ralrnmpo  6141  rexrnmpo  6142  ovid  6143  ov  6146  ovg  6166  ofrfval2  6257  fmpox  6370  1stconst  6391  2ndconst  6392  f1od2  6405  rbropapd  6413  brtpos2  6422  dfsmo2  6458  frecabcl  6570  brdifun  6734  eqerlem  6738  brecop  6799  erovlem  6801  mapsn  6864  mptelixpg  6908  map1  6992  xpsnen  7010  xpdom2  7020  xpf1o  7035  supubti  7203  infglbti  7229  ctssdccl  7315  nninfwlpoim  7383  nninfinfwlpo  7384  netap  7478  2omotaplemap  7481  ltpiord  7544  nlt1pig  7566  elinp  7699  ltdfpr  7731  genpassl  7749  genpassu  7750  1idprl  7815  1idpru  7816  gt0srpr  7973  mappsrprg  8029  map2psrprg  8030  peano2nnnn  8078  recidpirq  8083  axprecex  8105  xrlenlt  8249  addsubeq4  8399  renegcl  8445  lesub0  8664  recexaplem2  8837  conjmulap  8914  rerecclap  8915  creui  9145  peano2nn  9160  nndiv  9189  elznn0  9499  eqreznegel  9853  negelrp  9927  ltxr  10015  divelunit  10242  iccf1o  10244  elfz2  10255  elfzp1  10312  fzdifsuc  10321  fznn  10329  nelfzo  10392  fzosplitsni  10487  fvinim0ffz  10493  infssuzex  10499  zsupssdc  10504  frec2uzisod  10675  sq11i  10897  wrdval  11125  csbwrdg  11152  swrdnd  11249  wrd2ind  11313  cjreb  11449  rexfiuz  11572  cau3lem  11697  pwm1geoserap1  12092  mertensabs  12121  divides  12373  dvdsabseq  12431  odd2np1  12457  oddm1even  12459  modremain  12513  bezoutlemnewy  12590  bezoutlemstep  12591  bezoutlemmain  12592  bezoutlema  12593  bezoutlemb  12594  isprm2  12712  isprm4  12714  dvdsnprmd  12720  oddprmdvds  12950  4sqlem2  12985  4sqlem12  12998  xpsfrnel2  13452  issubm  13578  grplmulf1o  13680  grplactcnv  13708  issubg  13783  elnmz  13818  isghm  13853  ghmeqker  13881  srg1zr  14024  iscrng2  14052  issubrng  14237  aprval  14320  zndvds  14687  znleval  14691  psrbag  14707  istopg  14752  basgen2  14834  isnei  14897  restdis  14937  iscn  14950  iscnp  14952  lmbr2  14967  lmbrf  14968  txcn  15028  cnmpt21  15044  blres  15187  isxms2  15205  metrest  15259  metcnp  15265  txmetcnp  15271  txmetcn  15272  cnblcld  15288  reopnap  15299  ioocosf1o  15607  mpodvdsmulf1o  15743  gausslemma2dlem0i  15815  gausslemma2dlem1a  15816  lgseisenlem2  15829  lgsquadlem1  15835  lgsquadlem2  15836  2lgslem1a  15846  isuhgrm  15951  isushgrm  15952  isupgren  15975  isumgren  15985  isuspgren  16037  isusgren  16038  uhgr0v0e  16114  vtxdg0v  16174  iswlk  16203  wlk1walkdom  16239  istrl  16265  clwwlkn1  16298  clwwlkn2  16301  clwwlknonel  16312  clwwlknun  16321  iseupth  16327  eupthres  16337  eupth2lem1  16338  eupth2lemsfi  16358  bj-nn0sucALT  16633  apdiff  16719