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  1375  xordidc  1377  19.32dc  1657  r19.32vdc  2580  opbrop  4618  fvopab3g  5494  respreima  5548  fmptco  5586  cocan1  5688  cocan2  5689  brtposg  6151  nnmword  6414  swoer  6457  erth  6473  brecop  6519  ecopovsymg  6528  xpdom2  6725  ctssdccl  6996  pitric  7129  ltexpi  7145  ltapig  7146  ltmpig  7147  ltanqg  7208  ltmnqg  7209  enq0breq  7244  genpassl  7332  genpassu  7333  1idprl  7398  1idpru  7399  caucvgprlemcanl  7452  ltasrg  7578  prsrlt  7595  caucvgsrlemoffcau  7606  ltpsrprg  7611  map2psrprg  7613  axpre-ltadd  7694  subsub23  7967  leadd1  8192  lemul1  8355  reapmul1lem  8356  reapmul1  8357  reapadd1  8358  apsym  8368  apadd1  8370  apti  8384  apcon4bid  8386  lediv1  8627  lt2mul2div  8637  lerec  8642  ltdiv2  8645  lediv2  8649  le2msq  8659  avgle1  8960  avgle2  8961  nn01to3  9409  qapne  9431  cnref1o  9440  xleneg  9620  xsubge0  9664  xleaddadd  9670  iooneg  9771  iccneg  9772  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  fzsplit2  9830  fzaddel  9839  fzrev  9864  elfzo  9926  fzon  9943  elfzom1b  10006  ioo0  10037  ico0  10039  ioc0  10040  flqlt  10056  negqmod0  10104  frec2uzled  10202  expeq0  10324  nn0opthlem1d  10466  leisorel  10580  cjreb  10638  ltmininf  11006  minclpr  11008  xrmaxlesup  11028  xrltmininf  11039  xrminltinf  11041  tanaddaplem  11445  nndivdvds  11499  moddvds  11502  modmulconst  11525  oddm1even  11572  ltoddhalfle  11590  dvdssq  11719  phiprmpw  11898  cnrest2  12405  cnptoprest  12408  cnptoprest2  12409  lmss  12415  lmff  12418  txlm  12448  ismet2  12523  blres  12603  xmetec  12606  bdbl  12672  metrest  12675  cnbl0  12703  cnblcld  12704  reopnap  12707  bl2ioo  12711  limcdifap  12800