Theorem 3bitr4d 220

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)

Hypotheses

Ref	Expression
3bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3bitr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3bitr4d	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3bitr4d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3bitr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	bitr4d 191	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏))
5	1, 4	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:  ifpdfbidc  991  dfbi3dc  1439  xordidc  1441  19.32dc  1725  r19.32vdc  2680  opbrop  4795  fvopab3g  5700  respreima  5756  fmptco  5794  cocan1  5904  cocan2  5905  brtposg  6390  nnmword  6654  swoer  6698  erth  6716  brecop  6762  ecopovsymg  6771  xpdom2  6978  pw2f1odclem  6983  opabfi  7088  ctssdccl  7266  omniwomnimkv  7322  nninfwlporlemd  7327  pitric  7496  ltexpi  7512  ltapig  7513  ltmpig  7514  ltanqg  7575  ltmnqg  7576  enq0breq  7611  genpassl  7699  genpassu  7700  1idprl  7765  1idpru  7766  caucvgprlemcanl  7819  ltasrg  7945  prsrlt  7962  caucvgsrlemoffcau  7973  ltpsrprg  7978  map2psrprg  7980  axpre-ltadd  8061  subsub23  8339  leadd1  8565  lemul1  8728  reapmul1lem  8729  reapmul1  8730  reapadd1  8731  apsym  8741  apadd1  8743  apti  8757  apcon4bid  8759  lediv1  9004  lt2mul2div  9014  lerec  9019  ltdiv2  9022  lediv2  9026  le2msq  9036  avgle1  9340  avgle2  9341  nn01to3  9800  qapne  9822  cnref1o  9834  xleneg  10021  xsubge0  10065  xleaddadd  10071  iooneg  10172  iccneg  10173  iccshftr  10178  iccshftl  10180  iccdil  10182  icccntr  10184  fzsplit2  10234  fzaddel  10243  fzrev  10268  elfzo  10333  nelfzo  10336  fzon  10351  elfzom1b  10422  ioo0  10466  ico0  10468  ioc0  10469  flqlt  10490  negqmod0  10540  frec2uzled  10638  expeq0  10779  nn0leexp2  10919  nn0opthlem1d  10929  leisorel  11046  cjreb  11363  ltmininf  11732  minclpr  11734  xrmaxlesup  11756  xrltmininf  11767  xrminltinf  11769  tanaddaplem  12235  nndivdvds  12293  moddvds  12296  modmulconst  12320  oddm1even  12372  ltoddhalfle  12390  bitsp1  12448  dvdssq  12538  phiprmpw  12730  eulerthlemh  12739  odzdvds  12754  pc2dvds  12839  1arith  12876  issubg3  13715  eqgid  13749  resghm2b  13785  conjghm  13799  conjnmzb  13803  ablsubsub23  13848  issrgid  13930  isringid  13974  opprsubgg  14033  opprunitd  14059  crngunit  14060  unitpropdg  14097  issubrng  14148  opprsubrngg  14160  lsslss  14330  lsspropdg  14380  rspsn  14483  znidom  14606  cnrest2  14895  cnptoprest  14898  cnptoprest2  14899  lmss  14905  lmff  14908  txlm  14938  ismet2  15013  blres  15093  xmetec  15096  bdbl  15162  metrest  15165  cnbl0  15193  cnblcld  15194  reopnap  15205  bl2ioo  15209  limcdifap  15321  efle  15435  reapef  15437  logleb  15534  logrpap0b  15535  cxplt  15575  cxple  15576  rpcxple2  15577  rpcxplt2  15578  cxplt3  15579  cxple3  15580  apcxp2  15598  logbleb  15620  logblt  15621  lgsdilem  15691  lgsne0  15702  lgsquadlem1  15741  lgsquadlem2  15742  m1lgs  15749  2lgslem1a  15752  2lgs  15768  ausgrusgrben  15951  iooref1o  16333