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  4707  fvopab3g  5591  respreima  5646  fmptco  5684  cocan1  5790  cocan2  5791  brtposg  6257  nnmword  6521  swoer  6565  erth  6581  brecop  6627  ecopovsymg  6636  xpdom2  6833  ctssdccl  7112  omniwomnimkv  7167  nninfwlporlemd  7172  pitric  7322  ltexpi  7338  ltapig  7339  ltmpig  7340  ltanqg  7401  ltmnqg  7402  enq0breq  7437  genpassl  7525  genpassu  7526  1idprl  7591  1idpru  7592  caucvgprlemcanl  7645  ltasrg  7771  prsrlt  7788  caucvgsrlemoffcau  7799  ltpsrprg  7804  map2psrprg  7806  axpre-ltadd  7887  subsub23  8164  leadd1  8389  lemul1  8552  reapmul1lem  8553  reapmul1  8554  reapadd1  8555  apsym  8565  apadd1  8567  apti  8581  apcon4bid  8583  lediv1  8828  lt2mul2div  8838  lerec  8843  ltdiv2  8846  lediv2  8850  le2msq  8860  avgle1  9161  avgle2  9162  nn01to3  9619  qapne  9641  cnref1o  9652  xleneg  9839  xsubge0  9883  xleaddadd  9889  iooneg  9990  iccneg  9991  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  fzsplit2  10052  fzaddel  10061  fzrev  10086  elfzo  10151  fzon  10168  elfzom1b  10231  ioo0  10262  ico0  10264  ioc0  10265  flqlt  10285  negqmod0  10333  frec2uzled  10431  expeq0  10553  nn0leexp2  10692  nn0opthlem1d  10702  leisorel  10819  cjreb  10877  ltmininf  11245  minclpr  11247  xrmaxlesup  11269  xrltmininf  11280  xrminltinf  11282  tanaddaplem  11748  nndivdvds  11805  moddvds  11808  modmulconst  11832  oddm1even  11882  ltoddhalfle  11900  dvdssq  12034  phiprmpw  12224  eulerthlemh  12233  odzdvds  12247  pc2dvds  12331  1arith  12367  issubg3  13057  eqgid  13090  ablsubsub23  13133  issrgid  13169  isringid  13213  opprunitd  13284  crngunit  13285  unitpropdg  13322  lsslss  13473  cnrest2  13775  cnptoprest  13778  cnptoprest2  13779  lmss  13785  lmff  13788  txlm  13818  ismet2  13893  blres  13973  xmetec  13976  bdbl  14042  metrest  14045  cnbl0  14073  cnblcld  14074  reopnap  14077  bl2ioo  14081  limcdifap  14170  efle  14236  reapef  14238  logleb  14335  logrpap0b  14336  cxplt  14375  cxple  14376  rpcxple2  14377  rpcxplt2  14378  cxplt3  14379  cxple3  14380  apcxp2  14397  logbleb  14418  logblt  14419  lgsdilem  14467  lgsne0  14478  m1lgs  14491  iooref1o  14821