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  4800  fvopab3g  5712  respreima  5768  fmptco  5806  cocan1  5920  cocan2  5921  brtposg  6411  nnmword  6677  swoer  6721  erth  6739  brecop  6785  ecopovsymg  6794  xpdom2  7003  pw2f1odclem  7008  opabfi  7116  ctssdccl  7294  omniwomnimkv  7350  nninfwlporlemd  7355  pitric  7524  ltexpi  7540  ltapig  7541  ltmpig  7542  ltanqg  7603  ltmnqg  7604  enq0breq  7639  genpassl  7727  genpassu  7728  1idprl  7793  1idpru  7794  caucvgprlemcanl  7847  ltasrg  7973  prsrlt  7990  caucvgsrlemoffcau  8001  ltpsrprg  8006  map2psrprg  8008  axpre-ltadd  8089  subsub23  8367  leadd1  8593  lemul1  8756  reapmul1lem  8757  reapmul1  8758  reapadd1  8759  apsym  8769  apadd1  8771  apti  8785  apcon4bid  8787  lediv1  9032  lt2mul2div  9042  lerec  9047  ltdiv2  9050  lediv2  9054  le2msq  9064  avgle1  9368  avgle2  9369  nn01to3  9829  qapne  9851  cnref1o  9863  xleneg  10050  xsubge0  10094  xleaddadd  10100  iooneg  10201  iccneg  10202  iccshftr  10207  iccshftl  10209  iccdil  10211  icccntr  10213  fzsplit2  10263  fzaddel  10272  fzrev  10297  elfzo  10362  nelfzo  10365  fzon  10380  elfzom1b  10452  ioo0  10496  ico0  10498  ioc0  10499  flqlt  10520  negqmod0  10570  frec2uzled  10668  expeq0  10809  nn0leexp2  10949  nn0opthlem1d  10959  leisorel  11077  cjreb  11398  ltmininf  11767  minclpr  11769  xrmaxlesup  11791  xrltmininf  11802  xrminltinf  11804  tanaddaplem  12270  nndivdvds  12328  moddvds  12331  modmulconst  12355  oddm1even  12407  ltoddhalfle  12425  bitsp1  12483  dvdssq  12573  phiprmpw  12765  eulerthlemh  12774  odzdvds  12789  pc2dvds  12874  1arith  12911  issubg3  13750  eqgid  13784  resghm2b  13820  conjghm  13834  conjnmzb  13838  ablsubsub23  13883  issrgid  13965  isringid  14009  opprsubgg  14068  opprunitd  14095  crngunit  14096  unitpropdg  14133  issubrng  14184  opprsubrngg  14196  lsslss  14366  lsspropdg  14416  rspsn  14519  znidom  14642  cnrest2  14931  cnptoprest  14934  cnptoprest2  14935  lmss  14941  lmff  14944  txlm  14974  ismet2  15049  blres  15129  xmetec  15132  bdbl  15198  metrest  15201  cnbl0  15229  cnblcld  15230  reopnap  15241  bl2ioo  15245  limcdifap  15357  efle  15471  reapef  15473  logleb  15570  logrpap0b  15571  cxplt  15611  cxple  15612  rpcxple2  15613  rpcxplt2  15614  cxplt3  15615  cxple3  15616  apcxp2  15634  logbleb  15656  logblt  15657  lgsdilem  15727  lgsne0  15738  lgsquadlem1  15777  lgsquadlem2  15778  m1lgs  15785  2lgslem1a  15788  2lgs  15804  ausgrusgrben  15987  uspgr2wlkeq  16137  isclwwlknx  16184  iooref1o  16516