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	|- ( ph -> ( ps <-> ch ) )
3bitr4d.2	|- ( ph -> ( th <-> ps ) )
3bitr4d.3	|- ( ph -> ( ta <-> ch ) )

Assertion

Ref	Expression
3bitr4d	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
2		3bitr4d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3		3bitr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
4	2, 3	bitr4d 191	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 188	1 |- ( ph -> ( th <-> ta ) )

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  993  dfbi3dc  1441  xordidc  1443  19.32dc  1727  r19.32vdc  2682  opbrop  4805  fvopab3g  5719  respreima  5775  fmptco  5813  cocan1  5928  cocan2  5929  brtposg  6420  nnmword  6686  swoer  6730  erth  6748  brecop  6794  ecopovsymg  6803  xpdom2  7015  pw2f1odclem  7020  opabfi  7132  ctssdccl  7310  omniwomnimkv  7366  nninfwlporlemd  7371  pitric  7541  ltexpi  7557  ltapig  7558  ltmpig  7559  ltanqg  7620  ltmnqg  7621  enq0breq  7656  genpassl  7744  genpassu  7745  1idprl  7810  1idpru  7811  caucvgprlemcanl  7864  ltasrg  7990  prsrlt  8007  caucvgsrlemoffcau  8018  ltpsrprg  8023  map2psrprg  8025  axpre-ltadd  8106  subsub23  8384  leadd1  8610  lemul1  8773  reapmul1lem  8774  reapmul1  8775  reapadd1  8776  apsym  8786  apadd1  8788  apti  8802  apcon4bid  8804  lediv1  9049  lt2mul2div  9059  lerec  9064  ltdiv2  9067  lediv2  9071  le2msq  9081  avgle1  9385  avgle2  9386  nn01to3  9851  qapne  9873  cnref1o  9885  xleneg  10072  xsubge0  10116  xleaddadd  10122  iooneg  10223  iccneg  10224  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzsplit2  10285  fzaddel  10294  fzrev  10319  elfzo  10384  nelfzo  10387  fzon  10402  elfzom1b  10475  ioo0  10520  ico0  10522  ioc0  10523  flqlt  10544  negqmod0  10594  frec2uzled  10692  expeq0  10833  nn0leexp2  10973  nn0opthlem1d  10983  leisorel  11102  cjreb  11444  ltmininf  11813  minclpr  11815  xrmaxlesup  11837  xrltmininf  11848  xrminltinf  11850  tanaddaplem  12317  nndivdvds  12375  moddvds  12378  modmulconst  12402  oddm1even  12454  ltoddhalfle  12472  bitsp1  12530  dvdssq  12620  phiprmpw  12812  eulerthlemh  12821  odzdvds  12836  pc2dvds  12921  1arith  12958  issubg3  13797  eqgid  13831  resghm2b  13867  conjghm  13881  conjnmzb  13885  ablsubsub23  13930  issrgid  14013  isringid  14057  opprsubgg  14116  opprunitd  14143  crngunit  14144  unitpropdg  14181  issubrng  14232  opprsubrngg  14244  lsslss  14414  lsspropdg  14464  rspsn  14567  znidom  14690  cnrest2  14979  cnptoprest  14982  cnptoprest2  14983  lmss  14989  lmff  14992  txlm  15022  ismet2  15097  blres  15177  xmetec  15180  bdbl  15246  metrest  15249  cnbl0  15277  cnblcld  15278  reopnap  15289  bl2ioo  15293  limcdifap  15405  efle  15519  reapef  15521  logleb  15618  logrpap0b  15619  cxplt  15659  cxple  15660  rpcxple2  15661  rpcxplt2  15662  cxplt3  15663  cxple3  15664  apcxp2  15682  logbleb  15704  logblt  15705  lgsdilem  15775  lgsne0  15786  lgsquadlem1  15825  lgsquadlem2  15826  m1lgs  15833  2lgslem1a  15836  2lgs  15852  ausgrusgrben  16038  uspgr2wlkeq  16235  isclwwlknx  16286  eupth2lem3lem6fi  16341  iooref1o  16689