Theorem 3bitr4d 219

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 190	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏))
5	1, 4	bitrd 187	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dfbi3dc  1387  xordidc  1389  19.32dc  1667  r19.32vdc  2615  opbrop  4683  fvopab3g  5559  respreima  5613  fmptco  5651  cocan1  5755  cocan2  5756  brtposg  6222  nnmword  6486  swoer  6529  erth  6545  brecop  6591  ecopovsymg  6600  xpdom2  6797  ctssdccl  7076  omniwomnimkv  7131  pitric  7262  ltexpi  7278  ltapig  7279  ltmpig  7280  ltanqg  7341  ltmnqg  7342  enq0breq  7377  genpassl  7465  genpassu  7466  1idprl  7531  1idpru  7532  caucvgprlemcanl  7585  ltasrg  7711  prsrlt  7728  caucvgsrlemoffcau  7739  ltpsrprg  7744  map2psrprg  7746  axpre-ltadd  7827  subsub23  8103  leadd1  8328  lemul1  8491  reapmul1lem  8492  reapmul1  8493  reapadd1  8494  apsym  8504  apadd1  8506  apti  8520  apcon4bid  8522  lediv1  8764  lt2mul2div  8774  lerec  8779  ltdiv2  8782  lediv2  8786  le2msq  8796  avgle1  9097  avgle2  9098  nn01to3  9555  qapne  9577  cnref1o  9588  xleneg  9773  xsubge0  9817  xleaddadd  9823  iooneg  9924  iccneg  9925  iccshftr  9930  iccshftl  9932  iccdil  9934  icccntr  9936  fzsplit2  9985  fzaddel  9994  fzrev  10019  elfzo  10084  fzon  10101  elfzom1b  10164  ioo0  10195  ico0  10197  ioc0  10198  flqlt  10218  negqmod0  10266  frec2uzled  10364  expeq0  10486  nn0leexp2  10624  nn0opthlem1d  10633  leisorel  10750  cjreb  10808  ltmininf  11176  minclpr  11178  xrmaxlesup  11200  xrltmininf  11211  xrminltinf  11213  tanaddaplem  11679  nndivdvds  11736  moddvds  11739  modmulconst  11763  oddm1even  11812  ltoddhalfle  11830  dvdssq  11964  phiprmpw  12154  eulerthlemh  12163  odzdvds  12177  pc2dvds  12261  1arith  12297  cnrest2  12876  cnptoprest  12879  cnptoprest2  12880  lmss  12886  lmff  12889  txlm  12919  ismet2  12994  blres  13074  xmetec  13077  bdbl  13143  metrest  13146  cnbl0  13174  cnblcld  13175  reopnap  13178  bl2ioo  13182  limcdifap  13271  efle  13337  reapef  13339  logleb  13436  logrpap0b  13437  cxplt  13476  cxple  13477  rpcxple2  13478  rpcxplt2  13479  cxplt3  13480  cxple3  13481  apcxp2  13498  logbleb  13519  logblt  13520  lgsdilem  13568  lgsne0  13579  iooref1o  13913