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 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr2id  193  bitr3id  194  3bitr4g  223  imim21b  253  pm5.17dc  916  dn1dc  973  bilukdc  1445  nf4dc  1722  sbal1  2062  abbibcom  2352  abbib  2356  necon3abid  2459  necon3bid  2461  necon1abiidc  2480  r19.21t  2625  ceqsralt  2849  ceqsrexv  2956  ceqsrex2v  2958  elab2g  2973  elrabf  2980  eueq2dc  2999  euxfrdc  3012  eqreu  3018  reu8  3022  ru  3050  sbcralt  3128  sbcrext  3129  sbcne12g  3165  csbnestgf  3200  dfss4st  3464  rexsng  3750  ralprg  3760  rexprg  3761  difsn  3852  opthpr  3897  ralunsn  3923  dfiin2g  4045  iunxsng  4088  iunxsngf  4090  elpwuni  4102  pwnss  4296  exmid01  4335  opelopabt  4404  opelopabga  4405  brabga  4406  opelopabgf  4412  elsucg  4549  elsuc2g  4550  brab2a  4828  opeliunxp  4830  posng  4847  brab2ga  4850  csbdmg  4975  elrnmpt1  5033  elrnmptg  5034  eliniseg2  5167  poleloe  5187  elxp4  5275  elxp5  5276  cnvpom  5330  sbcfung  5401  dffun8  5405  fncnv  5447  fununi  5449  fnssresb  5495  fnimaeq0  5505  funcocnv2  5664  dffn5im  5748  funimass4  5753  fnsnfv  5762  dmfco  5773  fndmdif  5814  fndmin  5816  unpreima  5833  respreima  5836  fsn2  5882  fnressn  5901  fressnfv  5902  elunirn  5972  dff13  5974  fliftel  5999  isoini  6024  f1oiso  6032  riotaeqimp  6063  acexmid  6084  fnbrovb  6130  eloprabga  6175  resoprab2  6185  ralrnmpo  6203  rexrnmpo  6204  ovid  6205  ov  6208  ovg  6228  ofrfval2  6319  fmpox  6436  1stconst  6457  2ndconst  6458  f1od2  6471  rbropapd  6513  brtpos2  6522  dfsmo2  6558  frecabcl  6670  brdifun  6834  eqerlem  6838  brecop  6899  erovlem  6901  mapfset  6945  mapsnd  6970  mapsn  6972  mptelixpg  7016  map1  7101  xpsnen  7119  xpdom2  7129  xpf1o  7144  mapunen  7151  supubti  7340  infglbti  7366  ctssdccl  7452  nninfwlpoim  7520  nninfinfwlpo  7521  netap  7621  2omotaplemap  7624  ltpiord  7687  nlt1pig  7709  elinp  7842  ltdfpr  7874  genpassl  7892  genpassu  7893  1idprl  7958  1idpru  7959  gt0srpr  8116  mappsrprg  8172  map2psrprg  8173  peano2nnnn  8221  recidpirq  8226  axprecex  8248  xrlenlt  8391  addsubeq4  8543  renegcl  8589  lesub0  8809  recexaplem2  8983  conjmulap  9062  rerecclap  9063  creui  9293  peano2nn  9319  nndiv  9348  elznn0  9664  eqreznegel  10024  negelrp  10099  ltxr  10188  divelunit  10415  iccf1o  10418  elfz2  10429  elfzp1  10490  fzdifsuc  10499  fznn  10507  nelfzo  10570  fzosplitsni  10665  fvinim0ffz  10671  infssuzex  10677  zsupssdc  10684  frec2uzisod  10858  sq11i  11080  nn0sqdc  11161  wrdval  11322  csbwrdg  11349  swrdnd  11446  wrd2ind  11510  cjreb  11646  rexfiuz  11770  cau3lem  11896  pwm1geoserap1  12293  mertensabs  12322  divides  12574  dvdsabseq  12632  odd2np1  12658  oddm1even  12660  modremain  12714  bezoutlemnewy  12791  bezoutlemstep  12792  bezoutlemmain  12793  bezoutlema  12794  bezoutlemb  12795  isprm2  12913  isprm4  12915  dvdsnprmd  12921  nnmaxpw  12971  oddprmdvds  13155  4sqlem2  13190  4sqlem12  13203  xpsfrnel2  13718  issubm  13830  grplmulf1o  13930  grplactcnv  13958  issubg  14027  elnmz  14062  isghm  14097  ghmeqker  14125  rng1zrlem  14309  iscrng2  14370  issubrng  14558  aprval  14642  zndvds  15035  znleval  15039  psrbag  15104  istopg  15152  basgen2  15234  isnei  15297  restdis  15337  iscn  15350  iscnp  15352  lmbr2  15367  lmbrf  15368  txcn  15428  cnmpt21  15444  blres  15587  isxms2  15605  metrest  15659  metcnp  15665  txmetcnp  15671  txmetcn  15672  cnblcld  15688  reopnap  15699  ioocosf1o  16008  mpodvdsmulf1o  16206  gausslemma2dlem0i  16298  gausslemma2dlem1a  16299  lgseisenlem2  16312  lgsquadlem1  16318  lgsquadlem2  16319  2lgslem1a  16329  isuhgrm  16434  isushgrm  16435  isupgren  16458  isumgren  16468  isuspgren  16520  isusgren  16521  uhgr0v0e  16597  vtxdg0v  16657  iswlk  16686  wlk1walkdom  16722  istrl  16748  clwwlkn1  16781  clwwlkn2  16784  clwwlknonel  16795  clwwlknun  16804  iseupth  16810  eupthres  16820  eupth2lem1  16821  eupth2lemsfi  16841  bj-nn0sucALT  17126  apdiff  17219  ralrals  17271  rexrals  17272  ralals  17277  rexals  17278