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:  ifpdfbidc  991  dfbi3dc  1439  xordidc  1441  19.32dc  1725  r19.32vdc  2680  opbrop  4803  fvopab3g  5715  respreima  5771  fmptco  5809  cocan1  5923  cocan2  5924  brtposg  6415  nnmword  6681  swoer  6725  erth  6743  brecop  6789  ecopovsymg  6798  xpdom2  7010  pw2f1odclem  7015  opabfi  7123  ctssdccl  7301  omniwomnimkv  7357  nninfwlporlemd  7362  pitric  7531  ltexpi  7547  ltapig  7548  ltmpig  7549  ltanqg  7610  ltmnqg  7611  enq0breq  7646  genpassl  7734  genpassu  7735  1idprl  7800  1idpru  7801  caucvgprlemcanl  7854  ltasrg  7980  prsrlt  7997  caucvgsrlemoffcau  8008  ltpsrprg  8013  map2psrprg  8015  axpre-ltadd  8096  subsub23  8374  leadd1  8600  lemul1  8763  reapmul1lem  8764  reapmul1  8765  reapadd1  8766  apsym  8776  apadd1  8778  apti  8792  apcon4bid  8794  lediv1  9039  lt2mul2div  9049  lerec  9054  ltdiv2  9057  lediv2  9061  le2msq  9071  avgle1  9375  avgle2  9376  nn01to3  9841  qapne  9863  cnref1o  9875  xleneg  10062  xsubge0  10106  xleaddadd  10112  iooneg  10213  iccneg  10214  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  fzsplit2  10275  fzaddel  10284  fzrev  10309  elfzo  10374  nelfzo  10377  fzon  10392  elfzom1b  10464  ioo0  10509  ico0  10511  ioc0  10512  flqlt  10533  negqmod0  10583  frec2uzled  10681  expeq0  10822  nn0leexp2  10962  nn0opthlem1d  10972  leisorel  11091  cjreb  11417  ltmininf  11786  minclpr  11788  xrmaxlesup  11810  xrltmininf  11821  xrminltinf  11823  tanaddaplem  12289  nndivdvds  12347  moddvds  12350  modmulconst  12374  oddm1even  12426  ltoddhalfle  12444  bitsp1  12502  dvdssq  12592  phiprmpw  12784  eulerthlemh  12793  odzdvds  12808  pc2dvds  12893  1arith  12930  issubg3  13769  eqgid  13803  resghm2b  13839  conjghm  13853  conjnmzb  13857  ablsubsub23  13902  issrgid  13984  isringid  14028  opprsubgg  14087  opprunitd  14114  crngunit  14115  unitpropdg  14152  issubrng  14203  opprsubrngg  14215  lsslss  14385  lsspropdg  14435  rspsn  14538  znidom  14661  cnrest2  14950  cnptoprest  14953  cnptoprest2  14954  lmss  14960  lmff  14963  txlm  14993  ismet2  15068  blres  15148  xmetec  15151  bdbl  15217  metrest  15220  cnbl0  15248  cnblcld  15249  reopnap  15260  bl2ioo  15264  limcdifap  15376  efle  15490  reapef  15492  logleb  15589  logrpap0b  15590  cxplt  15630  cxple  15631  rpcxple2  15632  rpcxplt2  15633  cxplt3  15634  cxple3  15635  apcxp2  15653  logbleb  15675  logblt  15676  lgsdilem  15746  lgsne0  15757  lgsquadlem1  15796  lgsquadlem2  15797  m1lgs  15804  2lgslem1a  15807  2lgs  15823  ausgrusgrben  16007  uspgr2wlkeq  16162  isclwwlknx  16211  iooref1o  16574