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  1379  xordidc  1381  19.32dc  1659  r19.32vdc  2606  opbrop  4664  fvopab3g  5540  respreima  5594  fmptco  5632  cocan1  5734  cocan2  5735  brtposg  6198  nnmword  6462  swoer  6505  erth  6521  brecop  6567  ecopovsymg  6576  xpdom2  6773  ctssdccl  7049  omniwomnimkv  7104  pitric  7235  ltexpi  7251  ltapig  7252  ltmpig  7253  ltanqg  7314  ltmnqg  7315  enq0breq  7350  genpassl  7438  genpassu  7439  1idprl  7504  1idpru  7505  caucvgprlemcanl  7558  ltasrg  7684  prsrlt  7701  caucvgsrlemoffcau  7712  ltpsrprg  7717  map2psrprg  7719  axpre-ltadd  7800  subsub23  8074  leadd1  8299  lemul1  8462  reapmul1lem  8463  reapmul1  8464  reapadd1  8465  apsym  8475  apadd1  8477  apti  8491  apcon4bid  8493  lediv1  8734  lt2mul2div  8744  lerec  8749  ltdiv2  8752  lediv2  8756  le2msq  8766  avgle1  9067  avgle2  9068  nn01to3  9519  qapne  9541  cnref1o  9552  xleneg  9734  xsubge0  9778  xleaddadd  9784  iooneg  9885  iccneg  9886  iccshftr  9891  iccshftl  9893  iccdil  9895  icccntr  9897  fzsplit2  9945  fzaddel  9954  fzrev  9979  elfzo  10041  fzon  10058  elfzom1b  10121  ioo0  10152  ico0  10154  ioc0  10155  flqlt  10175  negqmod0  10223  frec2uzled  10321  expeq0  10443  nn0opthlem1d  10587  leisorel  10701  cjreb  10759  ltmininf  11127  minclpr  11129  xrmaxlesup  11149  xrltmininf  11160  xrminltinf  11162  tanaddaplem  11628  nndivdvds  11685  moddvds  11688  modmulconst  11711  oddm1even  11758  ltoddhalfle  11776  dvdssq  11906  phiprmpw  12085  eulerthlemh  12094  cnrest2  12607  cnptoprest  12610  cnptoprest2  12611  lmss  12617  lmff  12620  txlm  12650  ismet2  12725  blres  12805  xmetec  12808  bdbl  12874  metrest  12877  cnbl0  12905  cnblcld  12906  reopnap  12909  bl2ioo  12913  limcdifap  13002  efle  13068  reapef  13070  logleb  13167  logrpap0b  13168  cxplt  13207  cxple  13208  rpcxple2  13209  rpcxplt2  13210  cxplt3  13211  cxple3  13212  apcxp2  13229  logbleb  13249  logblt  13250  iooref1o  13576