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  908  dn1dc  965  bilukdc  1418  nf4dc  1696  sbal1  2033  abbi  2323  necon3abid  2419  necon3bid  2421  necon1abiidc  2440  r19.21t  2585  ceqsralt  2807  ceqsrexv  2913  ceqsrex2v  2915  elab2g  2930  elrabf  2937  eueq2dc  2956  euxfrdc  2969  eqreu  2975  reu8  2979  ru  3007  sbcralt  3085  sbcrext  3086  sbcne12g  3122  csbnestgf  3157  dfss4st  3417  rexsng  3687  ralprg  3697  rexprg  3698  difsn  3784  opthpr  3829  ralunsn  3855  dfiin2g  3977  iunxsng  4020  iunxsngf  4022  elpwuni  4034  pwnss  4222  exmid01  4261  opelopabt  4329  opelopabga  4330  brabga  4331  opelopabgf  4337  elsucg  4472  elsuc2g  4473  brab2a  4749  opeliunxp  4751  posng  4768  brab2ga  4771  csbdmg  4894  elrnmpt1  4951  elrnmptg  4952  eliniseg2  5084  poleloe  5104  elxp4  5192  elxp5  5193  cnvpom  5247  sbcfung  5318  dffun8  5322  fncnv  5363  fununi  5365  fnssresb  5411  fnimaeq0  5421  funcocnv2  5573  dffn5im  5652  funimass4  5657  fnsnfv  5666  dmfco  5675  fndmdif  5713  fndmin  5715  unpreima  5733  respreima  5736  fsn2  5782  fnressn  5798  fressnfv  5799  elunirn  5863  dff13  5865  fliftel  5890  isoini  5915  f1oiso  5923  riotaeqimp  5952  acexmid  5973  eloprabga  6062  resoprab2  6072  ralrnmpo  6090  rexrnmpo  6091  ovid  6092  ov  6095  ovg  6115  ofrfval2  6205  fmpox  6316  1stconst  6337  2ndconst  6338  f1od2  6351  rbropapd  6358  brtpos2  6367  dfsmo2  6403  frecabcl  6515  brdifun  6677  eqerlem  6681  brecop  6742  erovlem  6744  mapsn  6807  mptelixpg  6851  map1  6935  xpsnen  6948  xpdom2  6958  xpf1o  6973  supubti  7134  infglbti  7160  ctssdccl  7246  nninfwlpoim  7314  nninfinfwlpo  7315  netap  7408  2omotaplemap  7411  ltpiord  7474  nlt1pig  7496  elinp  7629  ltdfpr  7661  genpassl  7679  genpassu  7680  1idprl  7745  1idpru  7746  gt0srpr  7903  mappsrprg  7959  map2psrprg  7960  peano2nnnn  8008  recidpirq  8013  axprecex  8035  xrlenlt  8179  addsubeq4  8329  renegcl  8375  lesub0  8594  recexaplem2  8767  conjmulap  8844  rerecclap  8845  creui  9075  peano2nn  9090  nndiv  9119  elznn0  9429  eqreznegel  9777  negelrp  9851  ltxr  9939  divelunit  10166  iccf1o  10168  elfz2  10179  elfzp1  10236  fzdifsuc  10245  fznn  10253  nelfzo  10316  fzosplitsni  10408  fvinim0ffz  10414  infssuzex  10420  zsupssdc  10425  frec2uzisod  10596  sq11i  10818  wrdval  11041  csbwrdg  11067  swrdnd  11157  wrd2ind  11221  cjreb  11343  rexfiuz  11466  cau3lem  11591  pwm1geoserap1  11985  mertensabs  12014  divides  12266  dvdsabseq  12324  odd2np1  12350  oddm1even  12352  modremain  12406  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlemmain  12485  bezoutlema  12486  bezoutlemb  12487  isprm2  12605  isprm4  12607  dvdsnprmd  12613  oddprmdvds  12843  4sqlem2  12878  4sqlem12  12891  xpsfrnel2  13345  issubm  13471  grplmulf1o  13573  grplactcnv  13601  issubg  13676  elnmz  13711  isghm  13746  ghmeqker  13774  srg1zr  13916  iscrng2  13944  issubrng  14128  aprval  14211  zndvds  14578  znleval  14582  psrbag  14598  istopg  14638  basgen2  14720  isnei  14783  restdis  14823  iscn  14836  iscnp  14838  lmbr2  14853  lmbrf  14854  txcn  14914  cnmpt21  14930  blres  15073  isxms2  15091  metrest  15145  metcnp  15151  txmetcnp  15157  txmetcn  15158  cnblcld  15174  reopnap  15185  ioocosf1o  15493  mpodvdsmulf1o  15629  gausslemma2dlem0i  15701  gausslemma2dlem1a  15702  lgseisenlem2  15715  lgsquadlem1  15721  lgsquadlem2  15722  2lgslem1a  15732  isuhgrm  15836  isushgrm  15837  isupgren  15860  isumgren  15870  isuspgren  15920  isusgren  15921  bj-nn0sucALT  16251  apdiff  16327