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:  dfbi3dc  1408  xordidc  1410  19.32dc  1693  r19.32vdc  2646  opbrop  4743  fvopab3g  5635  respreima  5691  fmptco  5729  cocan1  5835  cocan2  5836  brtposg  6313  nnmword  6577  swoer  6621  erth  6639  brecop  6685  ecopovsymg  6694  xpdom2  6891  pw2f1odclem  6896  opabfi  7000  ctssdccl  7178  omniwomnimkv  7234  nninfwlporlemd  7239  pitric  7390  ltexpi  7406  ltapig  7407  ltmpig  7408  ltanqg  7469  ltmnqg  7470  enq0breq  7505  genpassl  7593  genpassu  7594  1idprl  7659  1idpru  7660  caucvgprlemcanl  7713  ltasrg  7839  prsrlt  7856  caucvgsrlemoffcau  7867  ltpsrprg  7872  map2psrprg  7874  axpre-ltadd  7955  subsub23  8233  leadd1  8459  lemul1  8622  reapmul1lem  8623  reapmul1  8624  reapadd1  8625  apsym  8635  apadd1  8637  apti  8651  apcon4bid  8653  lediv1  8898  lt2mul2div  8908  lerec  8913  ltdiv2  8916  lediv2  8920  le2msq  8930  avgle1  9234  avgle2  9235  nn01to3  9693  qapne  9715  cnref1o  9727  xleneg  9914  xsubge0  9958  xleaddadd  9964  iooneg  10065  iccneg  10066  iccshftr  10071  iccshftl  10073  iccdil  10075  icccntr  10077  fzsplit2  10127  fzaddel  10136  fzrev  10161  elfzo  10226  nelfzo  10229  fzon  10244  elfzom1b  10307  ioo0  10351  ico0  10353  ioc0  10354  flqlt  10375  negqmod0  10425  frec2uzled  10523  expeq0  10664  nn0leexp2  10804  nn0opthlem1d  10814  leisorel  10931  cjreb  11033  ltmininf  11402  minclpr  11404  xrmaxlesup  11426  xrltmininf  11437  xrminltinf  11439  tanaddaplem  11905  nndivdvds  11963  moddvds  11966  modmulconst  11990  oddm1even  12042  ltoddhalfle  12060  bitsp1  12118  dvdssq  12208  phiprmpw  12400  eulerthlemh  12409  odzdvds  12424  pc2dvds  12509  1arith  12546  issubg3  13332  eqgid  13366  resghm2b  13402  conjghm  13416  conjnmzb  13420  ablsubsub23  13465  issrgid  13547  isringid  13591  opprsubgg  13650  opprunitd  13676  crngunit  13677  unitpropdg  13714  issubrng  13765  opprsubrngg  13777  lsslss  13947  lsspropdg  13997  rspsn  14100  znidom  14223  cnrest2  14482  cnptoprest  14485  cnptoprest2  14486  lmss  14492  lmff  14495  txlm  14525  ismet2  14600  blres  14680  xmetec  14683  bdbl  14749  metrest  14752  cnbl0  14780  cnblcld  14781  reopnap  14792  bl2ioo  14796  limcdifap  14908  efle  15022  reapef  15024  logleb  15121  logrpap0b  15122  cxplt  15162  cxple  15163  rpcxple2  15164  rpcxplt2  15165  cxplt3  15166  cxple3  15167  apcxp2  15185  logbleb  15207  logblt  15208  lgsdilem  15278  lgsne0  15289  lgsquadlem1  15328  lgsquadlem2  15329  m1lgs  15336  2lgslem1a  15339  2lgs  15355  iooref1o  15688