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:  dfbi3dc  1397  xordidc  1399  19.32dc  1679  r19.32vdc  2626  opbrop  4705  fvopab3g  5589  respreima  5644  fmptco  5682  cocan1  5787  cocan2  5788  brtposg  6254  nnmword  6518  swoer  6562  erth  6578  brecop  6624  ecopovsymg  6633  xpdom2  6830  ctssdccl  7109  omniwomnimkv  7164  nninfwlporlemd  7169  pitric  7319  ltexpi  7335  ltapig  7336  ltmpig  7337  ltanqg  7398  ltmnqg  7399  enq0breq  7434  genpassl  7522  genpassu  7523  1idprl  7588  1idpru  7589  caucvgprlemcanl  7642  ltasrg  7768  prsrlt  7785  caucvgsrlemoffcau  7796  ltpsrprg  7801  map2psrprg  7803  axpre-ltadd  7884  subsub23  8161  leadd1  8386  lemul1  8549  reapmul1lem  8550  reapmul1  8551  reapadd1  8552  apsym  8562  apadd1  8564  apti  8578  apcon4bid  8580  lediv1  8825  lt2mul2div  8835  lerec  8840  ltdiv2  8843  lediv2  8847  le2msq  8857  avgle1  9158  avgle2  9159  nn01to3  9616  qapne  9638  cnref1o  9649  xleneg  9836  xsubge0  9880  xleaddadd  9886  iooneg  9987  iccneg  9988  iccshftr  9993  iccshftl  9995  iccdil  9997  icccntr  9999  fzsplit2  10049  fzaddel  10058  fzrev  10083  elfzo  10148  fzon  10165  elfzom1b  10228  ioo0  10259  ico0  10261  ioc0  10262  flqlt  10282  negqmod0  10330  frec2uzled  10428  expeq0  10550  nn0leexp2  10689  nn0opthlem1d  10699  leisorel  10816  cjreb  10874  ltmininf  11242  minclpr  11244  xrmaxlesup  11266  xrltmininf  11277  xrminltinf  11279  tanaddaplem  11745  nndivdvds  11802  moddvds  11805  modmulconst  11829  oddm1even  11879  ltoddhalfle  11897  dvdssq  12031  phiprmpw  12221  eulerthlemh  12230  odzdvds  12244  pc2dvds  12328  1arith  12364  issubg3  13050  eqgid  13083  ablsubsub23  13126  issrgid  13162  isringid  13206  opprunitd  13277  crngunit  13278  unitpropdg  13315  cnrest2  13706  cnptoprest  13709  cnptoprest2  13710  lmss  13716  lmff  13719  txlm  13749  ismet2  13824  blres  13904  xmetec  13907  bdbl  13973  metrest  13976  cnbl0  14004  cnblcld  14005  reopnap  14008  bl2ioo  14012  limcdifap  14101  efle  14167  reapef  14169  logleb  14266  logrpap0b  14267  cxplt  14306  cxple  14307  rpcxple2  14308  rpcxplt2  14309  cxplt3  14310  cxple3  14311  apcxp2  14328  logbleb  14349  logblt  14350  lgsdilem  14398  lgsne0  14409  m1lgs  14422  iooref1o  14752