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

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:  bitr2di  197  bitr4di  198  3bitr3g  222  bibi2i  227  ibibr  246  biancomd  271  imanst  890  pm5.75  965  xordidc  1419  19.17  1580  alexdc  1643  nf4dc  1694  abeq2d  2320  cbvralf  2733  cbvrexf  2734  cbvreu  2740  cbvrab  2774  ceqsralt  2804  ralab2  2944  rexab2  2946  euxfr2dc  2965  reu7  2975  reu8  2976  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  ralss  3267  rexss  3268  elif  3591  prssg  3801  2ralunsn  3853  eluniab  3876  elintab  3910  dfiun2g  3973  dfiin2g  3974  cbvopab1  4133  cbvmpt  4155  axsep2  4179  bnd2  4233  opeqsn  4315  reusv3  4525  tfisi  4653  opeliunxp  4748  eliunxp  4835  relop  4846  eldm2g  4893  reldm0  4915  relrn0  4959  restidsing  5034  xpmlem  5122  elxp5  5190  cnvpom  5244  cbviota  5256  iota1  5265  sniota  5281  fncnv  5359  fnres  5412  brprcneu  5592  fnopfvb  5643  fvelrnb  5649  fvelimab  5658  fvopab3g  5675  eqfnfv3  5702  eqfnfv2f  5704  fvreseq  5706  fnreseql  5713  rexsupp  5727  respreima  5731  rexrn  5740  ralrn  5741  f1ompt  5754  fsn  5775  fconstfvm  5825  fconst3m  5826  fconst4m  5827  foima2  5843  rexima  5846  ralima  5847  dff13  5860  foeqcnvco  5882  fliftfun  5888  isocnv  5903  isoini  5910  f1oiso  5918  cbvriota  5933  eusvobj2  5953  oprabid  5999  eloprabga  6055  resoprab  6064  eqfnov  6075  eqfnov2  6076  ov6g  6107  funimassov  6119  ovelimab  6120  caovord2  6142  uchoice  6246  releldm2  6294  dfoprab4  6301  xporderlem  6340  poxp  6341  f1od2  6344  mpoxopovel  6350  brtpos2  6360  brtpos0  6361  rntpos  6366  dftpos3  6371  tpostpos  6373  tpossym  6385  tposoprab  6389  tfrcllemres  6471  frecabcl  6508  frecsuclem  6515  erth2  6690  qliftfun  6727  erovlem  6737  ecopovsym  6741  ecopovsymg  6744  th3qlem1  6747  mapdm0  6773  elpmg  6774  elpm2g  6775  map0e  6796  dom2lem  6886  mapsnen  6927  xpdom2  6951  xpf1o  6966  mapen  6968  ssfilem  6998  diffitest  7010  ac6sfi  7021  ss1o0el1o  7036  isoti  7135  cnvti  7147  omp1eomlem  7222  ismkvnex  7283  nninfwlporlemd  7300  en2prde  7327  netap  7401  2omotaplemap  7404  ltexpi  7485  ordpipqqs  7522  ltexnqq  7556  enq0enq  7579  enq0sym  7580  enq0tr  7582  nqnq0pi  7586  genipv  7657  genprndl  7669  genprndu  7670  genpdisj  7671  genpassl  7672  genpassu  7673  addcomprg  7726  mulcomprg  7728  ltnqpr  7741  ltnqpri  7742  ltexprlemm  7748  ltexprlemdisj  7754  suplocexprlemmu  7866  suplocexprlemdisj  7868  ltsrprg  7895  mulgt0sr  7926  elreal2  7978  ltresr  7987  ltresr2  7988  axprecex  8028  axpre-ltadd  8034  axpre-mulgt0  8035  axpre-mulext  8036  axpre-suploclemres  8049  subcan2  8332  negcon1  8359  negcon2  8360  lt0neg1  8576  lt0neg2  8577  le0neg1  8578  le0neg2  8579  reapirr  8685  reapmul1  8703  reapneg  8705  remulext1  8707  apti  8730  negap0  8738  divmulap2  8784  reclt1  9004  recgt1  9005  suprleubex  9062  addltmul  9309  elznn0  9422  zapne  9482  zltlen  9486  nn0lt10b  9488  nn0lt2  9489  eluz1  9687  raluz  9734  rexuz  9736  qltlen  9796  cnref1o  9807  rpnegap  9843  ltxr  9932  xlt0neg1  9995  xlt0neg2  9996  xle0neg1  9997  xle0neg2  9998  elixx1  10054  elixx3g  10058  elioo2  10078  icc0r  10083  elicc4  10097  elioopnf  10124  elioomnf  10125  iooneg  10145  iccneg  10146  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  iccf1o  10161  elfz1  10170  0fz1  10202  fzpr  10234  fzdifsuc  10238  uzsplit  10249  elfzm1b  10255  elfzp12  10256  fznn0  10270  exfzdc  10406  zsupcllemstep  10409  flqeqceilz  10500  zmodid2  10534  expap0  10751  qsqeqor  10832  bernneq  10842  hasheqf1o  10967  hashfacen  11018  ccatrn  11103  pfxsuffeqwrdeq  11189  wrd2ind  11214  sqrtmsq2i  11561  maxclpr  11648  minmax  11656  xrmaxlesup  11685  xrnegiso  11688  xrnegcon1d  11690  xrminmax  11691  clim0  11711  climrecvg1n  11774  summodc  11809  fsumsplit  11833  mertenslem2  11962  prodmodc  12004  fprodsplitdc  12022  fprod2dlemstep  12048  dvdsval2  12216  odd2np1lem  12298  even2n  12300  divalgb  12351  divalgmod  12353  bitsval  12369  bitsmod  12382  gcddvds  12399  bezoutlemmain  12434  nnwofdc  12474  isprm3  12555  prmind2  12557  dvdsprime  12559  coprm  12581  prmdvdsexp  12585  sqrt2irr  12599  sqpweven  12612  2sqpwodd  12613  pythagtriplem2  12704  pythagtrip  12721  pceu  12733  pc11  12769  elrest  13193  grpsubeq0  13533  grpsubadd  13535  issubg3  13643  isnsg  13653  eqger  13675  eqglact  13676  eqgid  13677  srgfcl  13850  dvdsrtr  13978  dvdsr02  13982  isunitd  13983  isrhm  14035  isrim0  14038  subsubrng2  14092  subsubrg2  14123  issubrg3  14124  opprdomnbg  14151  2idlelb  14382  mplelbascoe  14569  istopon  14600  isbasis2g  14632  isbasis3g  14633  tgss2  14666  bastop1  14670  iscld  14690  ntreq0  14719  restsn  14767  restopn2  14770  lmbr  14800  cnptoprest2  14827  txbas  14845  eltx  14846  txlm  14866  ishmeo  14891  hmeoimaf1o  14901  ispsmet  14910  ismet  14931  isxmet  14932  ismet2  14941  metn0  14965  elblps  14977  elbl  14978  bdbl  15090  qtopbasss  15108  elcncf  15160  ellimc3apf  15247  elply  15321  sincosq1sgn  15413  sincosq2sgn  15414  cos11  15440  logrpap0b  15463  lgsdir2lem4  15623  gausslemma2dlem0i  15649  lgsquadlem2  15670  m1lgs  15677  2lgsoddprmlem3  15703  2sqlem6  15712  2sqlem9  15716  2sqlem10  15717  2omap  16132  pw1map  16134  subctctexmid  16139  iooref1o  16175  iswomni0  16192