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	|- ( 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 190	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 187	1 |- ( ph -> ( th <-> ta ) )

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  1392  xordidc  1394  19.32dc  1672  r19.32vdc  2619  opbrop  4690  fvopab3g  5569  respreima  5624  fmptco  5662  cocan1  5766  cocan2  5767  brtposg  6233  nnmword  6497  swoer  6541  erth  6557  brecop  6603  ecopovsymg  6612  xpdom2  6809  ctssdccl  7088  omniwomnimkv  7143  nninfwlporlemd  7148  pitric  7283  ltexpi  7299  ltapig  7300  ltmpig  7301  ltanqg  7362  ltmnqg  7363  enq0breq  7398  genpassl  7486  genpassu  7487  1idprl  7552  1idpru  7553  caucvgprlemcanl  7606  ltasrg  7732  prsrlt  7749  caucvgsrlemoffcau  7760  ltpsrprg  7765  map2psrprg  7767  axpre-ltadd  7848  subsub23  8124  leadd1  8349  lemul1  8512  reapmul1lem  8513  reapmul1  8514  reapadd1  8515  apsym  8525  apadd1  8527  apti  8541  apcon4bid  8543  lediv1  8785  lt2mul2div  8795  lerec  8800  ltdiv2  8803  lediv2  8807  le2msq  8817  avgle1  9118  avgle2  9119  nn01to3  9576  qapne  9598  cnref1o  9609  xleneg  9794  xsubge0  9838  xleaddadd  9844  iooneg  9945  iccneg  9946  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  fzsplit2  10006  fzaddel  10015  fzrev  10040  elfzo  10105  fzon  10122  elfzom1b  10185  ioo0  10216  ico0  10218  ioc0  10219  flqlt  10239  negqmod0  10287  frec2uzled  10385  expeq0  10507  nn0leexp2  10645  nn0opthlem1d  10654  leisorel  10772  cjreb  10830  ltmininf  11198  minclpr  11200  xrmaxlesup  11222  xrltmininf  11233  xrminltinf  11235  tanaddaplem  11701  nndivdvds  11758  moddvds  11761  modmulconst  11785  oddm1even  11834  ltoddhalfle  11852  dvdssq  11986  phiprmpw  12176  eulerthlemh  12185  odzdvds  12199  pc2dvds  12283  1arith  12319  cnrest2  13030  cnptoprest  13033  cnptoprest2  13034  lmss  13040  lmff  13043  txlm  13073  ismet2  13148  blres  13228  xmetec  13231  bdbl  13297  metrest  13300  cnbl0  13328  cnblcld  13329  reopnap  13332  bl2ioo  13336  limcdifap  13425  efle  13491  reapef  13493  logleb  13590  logrpap0b  13591  cxplt  13630  cxple  13631  rpcxple2  13632  rpcxplt2  13633  cxplt3  13634  cxple3  13635  apcxp2  13652  logbleb  13673  logblt  13674  lgsdilem  13722  lgsne0  13733  iooref1o  14066