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  1408  xordidc  1410  19.32dc  1690  r19.32vdc  2643  opbrop  4739  fvopab3g  5631  respreima  5687  fmptco  5725  cocan1  5831  cocan2  5832  brtposg  6309  nnmword  6573  swoer  6617  erth  6635  brecop  6681  ecopovsymg  6690  xpdom2  6887  pw2f1odclem  6892  opabfi  6994  ctssdccl  7172  omniwomnimkv  7228  nninfwlporlemd  7233  pitric  7383  ltexpi  7399  ltapig  7400  ltmpig  7401  ltanqg  7462  ltmnqg  7463  enq0breq  7498  genpassl  7586  genpassu  7587  1idprl  7652  1idpru  7653  caucvgprlemcanl  7706  ltasrg  7832  prsrlt  7849  caucvgsrlemoffcau  7860  ltpsrprg  7865  map2psrprg  7867  axpre-ltadd  7948  subsub23  8226  leadd1  8451  lemul1  8614  reapmul1lem  8615  reapmul1  8616  reapadd1  8617  apsym  8627  apadd1  8629  apti  8643  apcon4bid  8645  lediv1  8890  lt2mul2div  8900  lerec  8905  ltdiv2  8908  lediv2  8912  le2msq  8922  avgle1  9226  avgle2  9227  nn01to3  9685  qapne  9707  cnref1o  9719  xleneg  9906  xsubge0  9950  xleaddadd  9956  iooneg  10057  iccneg  10058  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  fzsplit2  10119  fzaddel  10128  fzrev  10153  elfzo  10218  nelfzo  10221  fzon  10236  elfzom1b  10299  ioo0  10331  ico0  10333  ioc0  10334  flqlt  10355  negqmod0  10405  frec2uzled  10503  expeq0  10644  nn0leexp2  10784  nn0opthlem1d  10794  leisorel  10911  cjreb  11013  ltmininf  11381  minclpr  11383  xrmaxlesup  11405  xrltmininf  11416  xrminltinf  11418  tanaddaplem  11884  nndivdvds  11942  moddvds  11945  modmulconst  11969  oddm1even  12019  ltoddhalfle  12037  dvdssq  12171  phiprmpw  12363  eulerthlemh  12372  odzdvds  12386  pc2dvds  12471  1arith  12508  issubg3  13265  eqgid  13299  resghm2b  13335  conjghm  13349  conjnmzb  13353  ablsubsub23  13398  issrgid  13480  isringid  13524  opprsubgg  13583  opprunitd  13609  crngunit  13610  unitpropdg  13647  issubrng  13698  opprsubrngg  13710  lsslss  13880  lsspropdg  13930  rspsn  14033  znidom  14156  cnrest2  14415  cnptoprest  14418  cnptoprest2  14419  lmss  14425  lmff  14428  txlm  14458  ismet2  14533  blres  14613  xmetec  14616  bdbl  14682  metrest  14685  cnbl0  14713  cnblcld  14714  reopnap  14725  bl2ioo  14729  limcdifap  14841  efle  14952  reapef  14954  logleb  15051  logrpap0b  15052  cxplt  15091  cxple  15092  rpcxple2  15093  rpcxplt2  15094  cxplt3  15095  cxple3  15096  apcxp2  15113  logbleb  15134  logblt  15135  lgsdilem  15184  lgsne0  15195  lgsquadlem1  15234  lgsquadlem2  15235  m1lgs  15242  2lgslem1a  15245  2lgs  15261  iooref1o  15594