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  1417  xordidc  1419  19.32dc  1703  r19.32vdc  2657  opbrop  4772  fvopab3g  5675  respreima  5731  fmptco  5769  cocan1  5879  cocan2  5880  brtposg  6363  nnmword  6627  swoer  6671  erth  6689  brecop  6735  ecopovsymg  6744  xpdom2  6951  pw2f1odclem  6956  opabfi  7061  ctssdccl  7239  omniwomnimkv  7295  nninfwlporlemd  7300  pitric  7469  ltexpi  7485  ltapig  7486  ltmpig  7487  ltanqg  7548  ltmnqg  7549  enq0breq  7584  genpassl  7672  genpassu  7673  1idprl  7738  1idpru  7739  caucvgprlemcanl  7792  ltasrg  7918  prsrlt  7935  caucvgsrlemoffcau  7946  ltpsrprg  7951  map2psrprg  7953  axpre-ltadd  8034  subsub23  8312  leadd1  8538  lemul1  8701  reapmul1lem  8702  reapmul1  8703  reapadd1  8704  apsym  8714  apadd1  8716  apti  8730  apcon4bid  8732  lediv1  8977  lt2mul2div  8987  lerec  8992  ltdiv2  8995  lediv2  8999  le2msq  9009  avgle1  9313  avgle2  9314  nn01to3  9773  qapne  9795  cnref1o  9807  xleneg  9994  xsubge0  10038  xleaddadd  10044  iooneg  10145  iccneg  10146  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  fzsplit2  10207  fzaddel  10216  fzrev  10241  elfzo  10306  nelfzo  10309  fzon  10324  elfzom1b  10395  ioo0  10439  ico0  10441  ioc0  10442  flqlt  10463  negqmod0  10513  frec2uzled  10611  expeq0  10752  nn0leexp2  10892  nn0opthlem1d  10902  leisorel  11019  cjreb  11292  ltmininf  11661  minclpr  11663  xrmaxlesup  11685  xrltmininf  11696  xrminltinf  11698  tanaddaplem  12164  nndivdvds  12222  moddvds  12225  modmulconst  12249  oddm1even  12301  ltoddhalfle  12319  bitsp1  12377  dvdssq  12467  phiprmpw  12659  eulerthlemh  12668  odzdvds  12683  pc2dvds  12768  1arith  12805  issubg3  13643  eqgid  13677  resghm2b  13713  conjghm  13727  conjnmzb  13731  ablsubsub23  13776  issrgid  13858  isringid  13902  opprsubgg  13961  opprunitd  13987  crngunit  13988  unitpropdg  14025  issubrng  14076  opprsubrngg  14088  lsslss  14258  lsspropdg  14308  rspsn  14411  znidom  14534  cnrest2  14823  cnptoprest  14826  cnptoprest2  14827  lmss  14833  lmff  14836  txlm  14866  ismet2  14941  blres  15021  xmetec  15024  bdbl  15090  metrest  15093  cnbl0  15121  cnblcld  15122  reopnap  15133  bl2ioo  15137  limcdifap  15249  efle  15363  reapef  15365  logleb  15462  logrpap0b  15463  cxplt  15503  cxple  15504  rpcxple2  15505  rpcxplt2  15506  cxplt3  15507  cxple3  15508  apcxp2  15526  logbleb  15548  logblt  15549  lgsdilem  15619  lgsne0  15630  lgsquadlem1  15669  lgsquadlem2  15670  m1lgs  15677  2lgslem1a  15680  2lgs  15696  iooref1o  16175