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  1408  xordidc  1410  19.32dc  1693  r19.32vdc  2646  opbrop  4743  fvopab3g  5637  respreima  5693  fmptco  5731  cocan1  5837  cocan2  5838  brtposg  6321  nnmword  6585  swoer  6629  erth  6647  brecop  6693  ecopovsymg  6702  xpdom2  6899  pw2f1odclem  6904  opabfi  7008  ctssdccl  7186  omniwomnimkv  7242  nninfwlporlemd  7247  pitric  7407  ltexpi  7423  ltapig  7424  ltmpig  7425  ltanqg  7486  ltmnqg  7487  enq0breq  7522  genpassl  7610  genpassu  7611  1idprl  7676  1idpru  7677  caucvgprlemcanl  7730  ltasrg  7856  prsrlt  7873  caucvgsrlemoffcau  7884  ltpsrprg  7889  map2psrprg  7891  axpre-ltadd  7972  subsub23  8250  leadd1  8476  lemul1  8639  reapmul1lem  8640  reapmul1  8641  reapadd1  8642  apsym  8652  apadd1  8654  apti  8668  apcon4bid  8670  lediv1  8915  lt2mul2div  8925  lerec  8930  ltdiv2  8933  lediv2  8937  le2msq  8947  avgle1  9251  avgle2  9252  nn01to3  9710  qapne  9732  cnref1o  9744  xleneg  9931  xsubge0  9975  xleaddadd  9981  iooneg  10082  iccneg  10083  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  fzsplit2  10144  fzaddel  10153  fzrev  10178  elfzo  10243  nelfzo  10246  fzon  10261  elfzom1b  10324  ioo0  10368  ico0  10370  ioc0  10371  flqlt  10392  negqmod0  10442  frec2uzled  10540  expeq0  10681  nn0leexp2  10821  nn0opthlem1d  10831  leisorel  10948  cjreb  11050  ltmininf  11419  minclpr  11421  xrmaxlesup  11443  xrltmininf  11454  xrminltinf  11456  tanaddaplem  11922  nndivdvds  11980  moddvds  11983  modmulconst  12007  oddm1even  12059  ltoddhalfle  12077  bitsp1  12135  dvdssq  12225  phiprmpw  12417  eulerthlemh  12426  odzdvds  12441  pc2dvds  12526  1arith  12563  issubg3  13400  eqgid  13434  resghm2b  13470  conjghm  13484  conjnmzb  13488  ablsubsub23  13533  issrgid  13615  isringid  13659  opprsubgg  13718  opprunitd  13744  crngunit  13745  unitpropdg  13782  issubrng  13833  opprsubrngg  13845  lsslss  14015  lsspropdg  14065  rspsn  14168  znidom  14291  cnrest2  14580  cnptoprest  14583  cnptoprest2  14584  lmss  14590  lmff  14593  txlm  14623  ismet2  14698  blres  14778  xmetec  14781  bdbl  14847  metrest  14850  cnbl0  14878  cnblcld  14879  reopnap  14890  bl2ioo  14894  limcdifap  15006  efle  15120  reapef  15122  logleb  15219  logrpap0b  15220  cxplt  15260  cxple  15261  rpcxple2  15262  rpcxplt2  15263  cxplt3  15264  cxple3  15265  apcxp2  15283  logbleb  15305  logblt  15306  lgsdilem  15376  lgsne0  15387  lgsquadlem1  15426  lgsquadlem2  15427  m1lgs  15434  2lgslem1a  15437  2lgs  15453  iooref1o  15791