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  994  dfbi3dc  1442  xordidc  1444  19.32dc  1727  r19.32vdc  2694  opbrop  4834  fvopab3g  5755  respreima  5810  fmptco  5848  cocan1  5966  cocan2  5967  suppimacnvfn  6459  brtposg  6498  nnmword  6764  swoer  6808  erth  6826  brecop  6872  ecopovsymg  6881  xpdom2  7095  pw2f1odclem  7100  opabfi  7213  ctssdccl  7415  omniwomnimkv  7471  nninfwlporlemd  7476  pitric  7652  ltexpi  7668  ltapig  7669  ltmpig  7670  ltanqg  7731  ltmnqg  7732  enq0breq  7767  genpassl  7855  genpassu  7856  1idprl  7921  1idpru  7922  caucvgprlemcanl  7975  ltasrg  8101  prsrlt  8118  caucvgsrlemoffcau  8129  ltpsrprg  8134  map2psrprg  8136  axpre-ltadd  8217  subsub23  8494  leadd1  8721  lemul1  8884  reapmul1lem  8885  reapmul1  8886  reapadd1  8887  apsym  8897  apadd1  8899  apti  8913  apcon4bid  8915  lediv1  9160  lt2mul2div  9170  lerec  9175  ltdiv2  9178  lediv2  9182  le2msq  9192  avgle1  9496  avgle2  9497  nn01to3  9967  qapne  9989  cnref1o  10001  xleneg  10189  xsubge0  10233  xleaddadd  10239  iooneg  10340  iccneg  10341  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  fzsplit2  10404  fzaddel  10414  fzrev  10440  elfzo  10505  nelfzo  10508  fzon  10523  elfzom1b  10596  ioo0  10643  ico0  10645  ioc0  10646  flqlt  10667  negqmod0  10717  frec2uzled  10815  expeq0  10956  nn0leexp2  11097  nn0opthlem1d  11107  leisorel  11234  cjreb  11576  ltmininf  11945  minclpr  11947  xrmaxlesup  11969  xrltmininf  11980  xrminltinf  11982  tanaddaplem  12449  nndivdvds  12507  moddvds  12510  modmulconst  12534  oddm1even  12586  ltoddhalfle  12604  bitsp1  12662  dvdssq  12752  phiprmpw  12944  eulerthlemh  12953  odzdvds  12968  pc2dvds  13053  1arith  13090  issubg3  13993  eqgid  14027  resghm2b  14063  conjghm  14077  conjnmzb  14081  ablsubsub23  14126  issrgid  14209  isringid  14253  opprsubgg  14313  opprunitd  14340  crngunit  14341  unitpropdg  14378  issubrng  14430  opprsubrngg  14442  opprdrng  14543  lsslss  14641  lsspropdg  14691  rspsn  14794  znidom  14917  psrbagconf1o  14940  cnrest2  15213  cnptoprest  15216  cnptoprest2  15217  lmss  15223  lmff  15226  txlm  15256  ismet2  15331  blres  15411  xmetec  15414  bdbl  15480  metrest  15483  cnbl0  15511  cnblcld  15512  reopnap  15523  bl2ioo  15527  limcdifap  15639  efle  15753  reapef  15755  logleb  15852  logrpap0b  15853  cxplt  15893  cxple  15894  rpcxple2  15895  rpcxplt2  15896  cxplt3  15897  cxple3  15898  apcxp2  15916  logbleb  15938  logblt  15939  lgsdilem  16012  lgsne0  16023  lgsquadlem1  16062  lgsquadlem2  16063  m1lgs  16070  2lgslem1a  16073  2lgs  16089  ausgrusgrben  16275  uspgr2wlkeq  16472  isclwwlknx  16523  eupth2lem3lem6fi  16578  iooref1o  16930