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  1397  xordidc  1399  19.32dc  1679  r19.32vdc  2626  opbrop  4707  fvopab3g  5592  respreima  5647  fmptco  5685  cocan1  5791  cocan2  5792  brtposg  6258  nnmword  6522  swoer  6566  erth  6582  brecop  6628  ecopovsymg  6637  xpdom2  6834  ctssdccl  7113  omniwomnimkv  7168  nninfwlporlemd  7173  pitric  7323  ltexpi  7339  ltapig  7340  ltmpig  7341  ltanqg  7402  ltmnqg  7403  enq0breq  7438  genpassl  7526  genpassu  7527  1idprl  7592  1idpru  7593  caucvgprlemcanl  7646  ltasrg  7772  prsrlt  7789  caucvgsrlemoffcau  7800  ltpsrprg  7805  map2psrprg  7807  axpre-ltadd  7888  subsub23  8165  leadd1  8390  lemul1  8553  reapmul1lem  8554  reapmul1  8555  reapadd1  8556  apsym  8566  apadd1  8568  apti  8582  apcon4bid  8584  lediv1  8829  lt2mul2div  8839  lerec  8844  ltdiv2  8847  lediv2  8851  le2msq  8861  avgle1  9162  avgle2  9163  nn01to3  9620  qapne  9642  cnref1o  9653  xleneg  9840  xsubge0  9884  xleaddadd  9890  iooneg  9991  iccneg  9992  iccshftr  9997  iccshftl  9999  iccdil  10001  icccntr  10003  fzsplit2  10053  fzaddel  10062  fzrev  10087  elfzo  10152  fzon  10169  elfzom1b  10232  ioo0  10263  ico0  10265  ioc0  10266  flqlt  10286  negqmod0  10334  frec2uzled  10432  expeq0  10554  nn0leexp2  10693  nn0opthlem1d  10703  leisorel  10820  cjreb  10878  ltmininf  11246  minclpr  11248  xrmaxlesup  11270  xrltmininf  11281  xrminltinf  11283  tanaddaplem  11749  nndivdvds  11806  moddvds  11809  modmulconst  11833  oddm1even  11883  ltoddhalfle  11901  dvdssq  12035  phiprmpw  12225  eulerthlemh  12234  odzdvds  12248  pc2dvds  12332  1arith  12368  issubg3  13062  eqgid  13096  ablsubsub23  13139  issrgid  13175  isringid  13219  opprunitd  13290  crngunit  13291  unitpropdg  13328  lsslss  13479  lsspropdg  13529  cnrest2  13897  cnptoprest  13900  cnptoprest2  13901  lmss  13907  lmff  13910  txlm  13940  ismet2  14015  blres  14095  xmetec  14098  bdbl  14164  metrest  14167  cnbl0  14195  cnblcld  14196  reopnap  14199  bl2ioo  14203  limcdifap  14292  efle  14358  reapef  14360  logleb  14457  logrpap0b  14458  cxplt  14497  cxple  14498  rpcxple2  14499  rpcxplt2  14500  cxplt3  14501  cxple3  14502  apcxp2  14519  logbleb  14540  logblt  14541  lgsdilem  14589  lgsne0  14600  m1lgs  14613  iooref1o  14944