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  8495  leadd1  8722  lemul1  8885  reapmul1lem  8886  reapmul1  8887  reapadd1  8888  apsym  8898  apadd1  8900  apti  8914  apcon4bid  8916  lediv1  9163  lt2mul2div  9173  lerec  9178  ltdiv2  9181  lediv2  9185  le2msq  9195  avgle1  9499  avgle2  9500  nn01to3  9970  qapne  9992  cnref1o  10004  xleneg  10192  xsubge0  10236  xleaddadd  10242  iooneg  10343  iccneg  10344  iccshftr  10349  iccshftl  10351  iccdil  10353  icccntr  10355  fzsplit2  10407  fzaddel  10417  fzrev  10443  elfzo  10508  nelfzo  10511  fzon  10526  elfzom1b  10599  ioo0  10646  ico0  10648  ioc0  10649  flqlt  10670  negqmod0  10720  frec2uzled  10818  expeq0  10959  nn0leexp2  11100  nn0opthlem1d  11110  leisorel  11237  cjreb  11579  ltmininf  11949  minclpr  11951  xrmaxlesup  11973  xrltmininf  11984  xrminltinf  11986  tanaddaplem  12453  nndivdvds  12511  moddvds  12514  modmulconst  12538  oddm1even  12590  ltoddhalfle  12608  bitsp1  12666  dvdssq  12756  phiprmpw  12948  eulerthlemh  12957  odzdvds  12972  pc2dvds  13057  1arith  13094  issubg3  13949  eqgid  13983  resghm2b  14019  conjghm  14033  conjnmzb  14037  ablsubsub23  14082  issrgid  14228  isringid  14272  opprsubgg  14332  opprunitd  14359  crngunit  14360  unitpropdg  14397  issubrng  14449  opprsubrngg  14461  opprdrng  14562  lsslss  14659  lsspropdg  14709  rspsn  14812  znidom  14935  psrbagconf1o  14958  cnrest2  15231  cnptoprest  15234  cnptoprest2  15235  lmss  15241  lmff  15244  txlm  15274  ismet2  15349  blres  15429  xmetec  15432  bdbl  15498  metrest  15501  cnbl0  15529  cnblcld  15530  reopnap  15541  bl2ioo  15545  limcdifap  15657  efle  15771  reapef  15773  logleb  15870  logrpap0b  15871  cxplt  15911  cxple  15912  rpcxple2  15913  rpcxplt2  15914  cxplt3  15915  cxple3  15916  apcxp2  15934  logbleb  15956  logblt  15957  lgsdilem  16030  lgsne0  16041  lgsquadlem1  16080  lgsquadlem2  16081  m1lgs  16088  2lgslem1a  16091  2lgs  16107  ausgrusgrben  16293  uspgr2wlkeq  16490  isclwwlknx  16541  eupth2lem3lem6fi  16596  iooref1o  16958