Theorem bitrdi 196

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitrdi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitrdi.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
bitrdi	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitrdi.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	a1i 9	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 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:  bitr2di  197  bitr4di  198  3bitr3g  222  bibi2i  227  ibibr  246  biancomd  271  imanst  900  pm5.75  975  xordidc  1448  19.17  1609  alexdc  1672  nf4dc  1722  abeq2d  2351  eqabrd  2378  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvrab  2819  ceqsralt  2849  ralab2  2990  rexab2  2992  euxfr2dc  3011  reu7  3021  reu8  3022  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  ralss  3314  rexss  3315  sseq0b  3564  elif  3652  prssg  3872  2ralunsn  3924  eluniab  3947  elintab  3981  dfiun2g  4044  dfiin2g  4045  cbvopab1  4204  cbvmpt  4226  axsepg  4250  bnd2  4310  opeqsn  4393  reusv3  4606  tfisi  4734  opeliunxp  4830  eliunxp  4919  relop  4930  eldm2g  4977  reldm0  4999  relrn0  5044  restidsing  5119  xpmlem  5208  elxp5  5276  cnvpom  5330  cbviota  5342  iota1  5352  sniota  5368  fncnv  5447  fnres  5500  brprcneu  5688  fnopfvb  5742  fvelrnb  5750  fvelimab  5759  fvopab3g  5778  eqfnfv3  5808  eqfnfv2f  5810  fvreseq  5812  fnreseql  5819  respreima  5836  rexrn  5845  ralrn  5846  f1ompt  5859  fsn  5880  fconstfvm  5933  fconst3m  5934  fconst4m  5935  foima2  5957  rexima  5960  ralima  5961  dff13  5974  foeqcnvco  5996  fliftfun  6002  isocnv  6017  isoini  6024  f1oiso  6032  cbvriota  6050  riotaeqimp  6063  eusvobj2  6071  oprabid  6117  eloprabga  6175  resoprab  6184  eqfnov  6195  eqfnov2  6196  ov6g  6227  funimassov  6239  ovelimab  6240  caovord2  6262  uchoice  6371  releldm2  6419  dfoprab4  6426  xporderlem  6467  poxp  6468  f1od2  6471  elsuppfng  6482  elsuppfn  6483  rexsupp  6493  mpoxopovel  6512  brtpos2  6522  brtpos0  6523  rntpos  6528  dftpos3  6533  tpostpos  6535  tpossym  6547  tposoprab  6551  tfrcllemres  6633  frecabcl  6670  frecsuclem  6677  erth2  6854  qliftfun  6891  erovlem  6901  ecopovsym  6905  ecopovsymg  6908  th3qlem1  6911  mapdm0  6937  elpmg  6938  elpm2g  6939  map0e  6967  dom2lem  7058  mapsnend  7099  mapsnen  7100  xpdom2  7129  xpf1o  7144  mapen  7146  ssfilem  7177  ssfilemd  7179  diffitest  7191  ac6sfi  7202  eqsndc  7210  ss1o0el1o  7220  2omap  7318  isoti  7347  cnvti  7359  omp1eomlem  7434  ismkvnex  7495  nninfwlporlemd  7512  en2prde  7539  netap  7620  2omotaplemap  7623  ltexpi  7704  ordpipqqs  7741  ltexnqq  7775  enq0enq  7798  enq0sym  7799  enq0tr  7801  nqnq0pi  7805  genipv  7876  genprndl  7888  genprndu  7889  genpdisj  7890  genpassl  7891  genpassu  7892  addcomprg  7945  mulcomprg  7947  ltnqpr  7960  ltnqpri  7961  ltexprlemm  7967  ltexprlemdisj  7973  suplocexprlemmu  8085  suplocexprlemdisj  8087  ltsrprg  8114  mulgt0sr  8145  elreal2  8197  ltresr  8206  ltresr2  8207  axprecex  8247  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axpre-suploclemres  8268  subcan2  8551  negcon1  8578  negcon2  8579  lt0neg1  8796  lt0neg2  8797  le0neg1  8798  le0neg2  8799  reapirr  8906  reapmul1  8924  reapneg  8926  remulext1  8928  apti  8951  negap0  8959  divmulap2  9007  reclt1  9227  recgt1  9228  suprleubex  9285  addltmul  9544  elznn0  9661  zapne  9721  zltlen  9726  nn0lt10b  9728  nn0lt2  9729  eluz1  9927  raluz  9980  rexuz  9982  qltlen  10042  cnref1o  10053  rpnegap  10089  ltxr  10179  xlt0neg1  10242  xlt0neg2  10243  xle0neg1  10244  xle0neg2  10245  elixx1  10301  elixx3g  10305  elioo2  10325  icc0r  10330  elicc4  10344  elioopnf  10371  elioomnf  10372  iooneg  10392  iccneg  10393  iccshftr  10398  iccshftl  10400  iccdil  10402  icccntr  10404  iccf1o  10409  elfz1  10418  0fz1  10451  fzpr  10486  fzdifsuc  10490  uzsplit  10501  elfzm1b  10507  elfzp12  10508  fznn0  10522  exfzdc  10661  zsupcllemstep  10664  flqeqceilz  10757  zmodid2  10791  expap0  11008  qsqeqor  11089  bernneq  11100  hasheqf1o  11226  ssenneg  11282  hashfibclem  11284  hashfacen  11286  hashf1  11289  ccatrn  11379  pfxsuffeqwrdeq  11472  wrd2ind  11497  sqrtmsq2i  11903  maxclpr  11990  minmax  11998  xrmaxlesup  12027  xrnegiso  12030  xrnegcon1d  12032  xrminmax  12033  clim0  12053  climrecvg1n  12116  summodc  12152  fsumsplit  12176  mertenslem2  12305  prodmodc  12347  fprodsplitdc  12365  fprod2dlemstep  12391  dvdsval2  12559  odd2np1lem  12641  even2n  12643  divalgb  12694  divalgmod  12696  bitsval  12712  bitsmod  12725  gcddvds  12742  bezoutlemmain  12777  nnwofdc  12817  isprm3  12898  prmind2  12900  dvdsprime  12902  coprm  12924  prmdvdsexp  12928  sqrt2irr  12942  sqpweven  12955  2sqpwodd  12956  pythagtriplem2  13047  pythagtrip  13064  pceu  13076  pc11  13112  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemodife  13242  elrest  13602  grpsubeq0  13893  grpsubadd  13895  issubg3  13997  isnsg  14007  eqger  14029  eqglact  14030  eqgid  14031  srgfcl  14279  dvdsrtr  14410  dvdsr02  14414  isunitd  14415  isrhm  14467  isrim0  14470  subsubrng2  14525  subsubrg2  14556  issubrg3  14557  opprdomnbg  14585  2idlelb  14844  mplelbascoe  15085  istopon  15116  isbasis2g  15148  isbasis3g  15149  tgss2  15182  bastop1  15186  iscld  15206  ntreq0  15235  restsn  15283  restopn2  15286  lmbr  15316  cnptoprest2  15343  txbas  15361  eltx  15362  txlm  15382  ishmeo  15407  hmeoimaf1o  15417  ispsmet  15426  ismet  15447  isxmet  15448  ismet2  15457  metn0  15481  elblps  15493  elbl  15494  bdbl  15606  qtopbasss  15624  elcncf  15676  ellimc3apf  15763  elply  15837  efap1p  15882  sincosq1sgn  15930  sincosq2sgn  15931  cos11  15957  logrpap0b  15981  lgsdir2lem4  16162  gausslemma2dlem0i  16188  lgsquadlem2  16209  m1lgs  16216  2lgsoddprmlem3  16242  2sqlem6  16251  2sqlem9  16255  2sqlem10  16256  vtxdfifiun  16550  wlkl1loop  16611  wlkv0  16622  wlklenvclwlk  16626  upgr2wlkdc  16630  isclwwlk  16647  isclwwlkng  16659  isclwwlknx  16669  clwwlkn2  16674  eupth2lem2dc  16712  eupth2lem3lem6fi  16724  pw1map  17037  subctctexmid  17042  iooref1o  17095  iswomni0  17113