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  1417  xordidc  1419  19.32dc  1703  r19.32vdc  2656  opbrop  4759  fvopab3g  5662  respreima  5718  fmptco  5756  cocan1  5866  cocan2  5867  brtposg  6350  nnmword  6614  swoer  6658  erth  6676  brecop  6722  ecopovsymg  6731  xpdom2  6938  pw2f1odclem  6943  opabfi  7047  ctssdccl  7225  omniwomnimkv  7281  nninfwlporlemd  7286  pitric  7447  ltexpi  7463  ltapig  7464  ltmpig  7465  ltanqg  7526  ltmnqg  7527  enq0breq  7562  genpassl  7650  genpassu  7651  1idprl  7716  1idpru  7717  caucvgprlemcanl  7770  ltasrg  7896  prsrlt  7913  caucvgsrlemoffcau  7924  ltpsrprg  7929  map2psrprg  7931  axpre-ltadd  8012  subsub23  8290  leadd1  8516  lemul1  8679  reapmul1lem  8680  reapmul1  8681  reapadd1  8682  apsym  8692  apadd1  8694  apti  8708  apcon4bid  8710  lediv1  8955  lt2mul2div  8965  lerec  8970  ltdiv2  8973  lediv2  8977  le2msq  8987  avgle1  9291  avgle2  9292  nn01to3  9751  qapne  9773  cnref1o  9785  xleneg  9972  xsubge0  10016  xleaddadd  10022  iooneg  10123  iccneg  10124  iccshftr  10129  iccshftl  10131  iccdil  10133  icccntr  10135  fzsplit2  10185  fzaddel  10194  fzrev  10219  elfzo  10284  nelfzo  10287  fzon  10302  elfzom1b  10371  ioo0  10415  ico0  10417  ioc0  10418  flqlt  10439  negqmod0  10489  frec2uzled  10587  expeq0  10728  nn0leexp2  10868  nn0opthlem1d  10878  leisorel  10995  cjreb  11227  ltmininf  11596  minclpr  11598  xrmaxlesup  11620  xrltmininf  11631  xrminltinf  11633  tanaddaplem  12099  nndivdvds  12157  moddvds  12160  modmulconst  12184  oddm1even  12236  ltoddhalfle  12254  bitsp1  12312  dvdssq  12402  phiprmpw  12594  eulerthlemh  12603  odzdvds  12618  pc2dvds  12703  1arith  12740  issubg3  13578  eqgid  13612  resghm2b  13648  conjghm  13662  conjnmzb  13666  ablsubsub23  13711  issrgid  13793  isringid  13837  opprsubgg  13896  opprunitd  13922  crngunit  13923  unitpropdg  13960  issubrng  14011  opprsubrngg  14023  lsslss  14193  lsspropdg  14243  rspsn  14346  znidom  14469  cnrest2  14758  cnptoprest  14761  cnptoprest2  14762  lmss  14768  lmff  14771  txlm  14801  ismet2  14876  blres  14956  xmetec  14959  bdbl  15025  metrest  15028  cnbl0  15056  cnblcld  15057  reopnap  15068  bl2ioo  15072  limcdifap  15184  efle  15298  reapef  15300  logleb  15397  logrpap0b  15398  cxplt  15438  cxple  15439  rpcxple2  15440  rpcxplt2  15441  cxplt3  15442  cxple3  15443  apcxp2  15461  logbleb  15483  logblt  15484  lgsdilem  15554  lgsne0  15565  lgsquadlem1  15604  lgsquadlem2  15605  m1lgs  15612  2lgslem1a  15615  2lgs  15631  iooref1o  16088