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  998  dfbi3dc  1446  xordidc  1448  19.32dc  1731  r19.32vdc  2700  opbrop  4852  fvopab3g  5775  respreima  5830  fmptco  5868  cocan1  5987  cocan2  5988  suppimacnvfn  6480  brtposg  6519  nnmword  6785  swoer  6829  erth  6847  brecop  6893  ecopovsymg  6902  xpdom2  7123  pw2f1odclem  7128  opabfi  7241  ctssdccl  7445  omniwomnimkv  7501  nninfwlporlemd  7506  pitric  7682  ltexpi  7698  ltapig  7699  ltmpig  7700  ltanqg  7761  ltmnqg  7762  enq0breq  7797  genpassl  7885  genpassu  7886  1idprl  7951  1idpru  7952  caucvgprlemcanl  8005  ltasrg  8131  prsrlt  8148  caucvgsrlemoffcau  8159  ltpsrprg  8164  map2psrprg  8166  axpre-ltadd  8247  subsub23  8525  leadd1  8752  lemul1  8915  reapmul1lem  8916  reapmul1  8917  reapadd1  8918  apsym  8928  apadd1  8930  apti  8944  apcon4bid  8946  lediv1  9193  lt2mul2div  9203  lerec  9208  ltdiv2  9211  lediv2  9215  le2msq  9225  avgle1  9529  avgle2  9530  nn01to3  10000  qapne  10022  cnref1o  10034  xleneg  10222  xsubge0  10266  xleaddadd  10272  iooneg  10373  iccneg  10374  iccshftr  10379  iccshftl  10381  iccdil  10383  icccntr  10385  fzsplit2  10438  fzaddel  10448  fzrev  10474  elfzo  10539  nelfzo  10542  fzon  10557  elfzom1b  10630  ioo0  10677  ico0  10679  ioc0  10680  flqlt  10701  negqmod0  10751  frec2uzled  10849  expeq0  10990  nn0leexp2  11131  nn0opthlem1d  11141  leisorel  11272  cjreb  11614  ltmininf  11984  minclpr  11986  xrmaxlesup  12008  xrltmininf  12019  xrminltinf  12021  tanaddaplem  12488  nndivdvds  12546  moddvds  12549  modmulconst  12573  oddm1even  12625  ltoddhalfle  12643  bitsp1  12701  dvdssq  12791  phiprmpw  12983  eulerthlemh  12992  odzdvds  13007  pc2dvds  13092  1arith  13129  issubg3  13978  eqgid  14012  resghm2b  14048  conjghm  14062  conjnmzb  14066  ablsubsub23  14112  issrgid  14268  isringid  14313  opprsubgg  14373  opprunitd  14400  crngunit  14401  unitpropdg  14438  issubrng  14490  opprsubrngg  14502  opprdrng  14603  lsslss  14701  lsspropdg  14751  rspsn  14854  znidom  14975  psrbagconf1o  15047  cnrest2  15320  cnptoprest  15323  cnptoprest2  15324  lmss  15330  lmff  15333  txlm  15363  ismet2  15438  blres  15518  xmetec  15521  bdbl  15587  metrest  15590  cnbl0  15618  cnblcld  15619  reopnap  15630  bl2ioo  15634  limcdifap  15746  efle  15860  reapef  15862  logleb  15959  logrpap0b  15960  cxplt  16001  cxple  16002  rpcxple2  16003  rpcxplt2  16004  cxplt3  16005  cxple3  16006  apcxp2  16024  logbleb  16046  logblt  16047  lgsdilem  16129  lgsne0  16140  lgsquadlem1  16179  lgsquadlem2  16180  m1lgs  16187  2lgslem1a  16190  2lgs  16206  ausgrusgrben  16392  uspgr2wlkeq  16589  isclwwlknx  16640  eupth2lem3lem6fi  16695  iooref1o  17057