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  1376  xordidc  1378  19.32dc  1658  r19.32vdc  2583  opbrop  4626  fvopab3g  5502  respreima  5556  fmptco  5594  cocan1  5696  cocan2  5697  brtposg  6159  nnmword  6422  swoer  6465  erth  6481  brecop  6527  ecopovsymg  6536  xpdom2  6733  ctssdccl  7004  omniwomnimkv  7049  pitric  7153  ltexpi  7169  ltapig  7170  ltmpig  7171  ltanqg  7232  ltmnqg  7233  enq0breq  7268  genpassl  7356  genpassu  7357  1idprl  7422  1idpru  7423  caucvgprlemcanl  7476  ltasrg  7602  prsrlt  7619  caucvgsrlemoffcau  7630  ltpsrprg  7635  map2psrprg  7637  axpre-ltadd  7718  subsub23  7991  leadd1  8216  lemul1  8379  reapmul1lem  8380  reapmul1  8381  reapadd1  8382  apsym  8392  apadd1  8394  apti  8408  apcon4bid  8410  lediv1  8651  lt2mul2div  8661  lerec  8666  ltdiv2  8669  lediv2  8673  le2msq  8683  avgle1  8984  avgle2  8985  nn01to3  9436  qapne  9458  cnref1o  9469  xleneg  9650  xsubge0  9694  xleaddadd  9700  iooneg  9801  iccneg  9802  iccshftr  9807  iccshftl  9809  iccdil  9811  icccntr  9813  fzsplit2  9861  fzaddel  9870  fzrev  9895  elfzo  9957  fzon  9974  elfzom1b  10037  ioo0  10068  ico0  10070  ioc0  10071  flqlt  10087  negqmod0  10135  frec2uzled  10233  expeq0  10355  nn0opthlem1d  10498  leisorel  10612  cjreb  10670  ltmininf  11038  minclpr  11040  xrmaxlesup  11060  xrltmininf  11071  xrminltinf  11073  tanaddaplem  11481  nndivdvds  11535  moddvds  11538  modmulconst  11561  oddm1even  11608  ltoddhalfle  11626  dvdssq  11755  phiprmpw  11934  cnrest2  12444  cnptoprest  12447  cnptoprest2  12448  lmss  12454  lmff  12457  txlm  12487  ismet2  12562  blres  12642  xmetec  12645  bdbl  12711  metrest  12714  cnbl0  12742  cnblcld  12743  reopnap  12746  bl2ioo  12750  limcdifap  12839  efle  12905  reapef  12907  logleb  13004  logrpap0b  13005  cxplt  13044  cxple  13045  rpcxple2  13046  rpcxplt2  13047  cxplt3  13048  cxple3  13049  apcxp2  13066  logbleb  13086  logblt  13087  iooref1o  13426