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  4797  fvopab3g  5706  respreima  5762  fmptco  5800  cocan1  5910  cocan2  5911  brtposg  6398  nnmword  6662  swoer  6706  erth  6724  brecop  6770  ecopovsymg  6779  xpdom2  6986  pw2f1odclem  6991  opabfi  7096  ctssdccl  7274  omniwomnimkv  7330  nninfwlporlemd  7335  pitric  7504  ltexpi  7520  ltapig  7521  ltmpig  7522  ltanqg  7583  ltmnqg  7584  enq0breq  7619  genpassl  7707  genpassu  7708  1idprl  7773  1idpru  7774  caucvgprlemcanl  7827  ltasrg  7953  prsrlt  7970  caucvgsrlemoffcau  7981  ltpsrprg  7986  map2psrprg  7988  axpre-ltadd  8069  subsub23  8347  leadd1  8573  lemul1  8736  reapmul1lem  8737  reapmul1  8738  reapadd1  8739  apsym  8749  apadd1  8751  apti  8765  apcon4bid  8767  lediv1  9012  lt2mul2div  9022  lerec  9027  ltdiv2  9030  lediv2  9034  le2msq  9044  avgle1  9348  avgle2  9349  nn01to3  9808  qapne  9830  cnref1o  9842  xleneg  10029  xsubge0  10073  xleaddadd  10079  iooneg  10180  iccneg  10181  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  fzsplit2  10242  fzaddel  10251  fzrev  10276  elfzo  10341  nelfzo  10344  fzon  10359  elfzom1b  10430  ioo0  10474  ico0  10476  ioc0  10477  flqlt  10498  negqmod0  10548  frec2uzled  10646  expeq0  10787  nn0leexp2  10927  nn0opthlem1d  10937  leisorel  11054  cjreb  11372  ltmininf  11741  minclpr  11743  xrmaxlesup  11765  xrltmininf  11776  xrminltinf  11778  tanaddaplem  12244  nndivdvds  12302  moddvds  12305  modmulconst  12329  oddm1even  12381  ltoddhalfle  12399  bitsp1  12457  dvdssq  12547  phiprmpw  12739  eulerthlemh  12748  odzdvds  12763  pc2dvds  12848  1arith  12885  issubg3  13724  eqgid  13758  resghm2b  13794  conjghm  13808  conjnmzb  13812  ablsubsub23  13857  issrgid  13939  isringid  13983  opprsubgg  14042  opprunitd  14068  crngunit  14069  unitpropdg  14106  issubrng  14157  opprsubrngg  14169  lsslss  14339  lsspropdg  14389  rspsn  14492  znidom  14615  cnrest2  14904  cnptoprest  14907  cnptoprest2  14908  lmss  14914  lmff  14917  txlm  14947  ismet2  15022  blres  15102  xmetec  15105  bdbl  15171  metrest  15174  cnbl0  15202  cnblcld  15203  reopnap  15214  bl2ioo  15218  limcdifap  15330  efle  15444  reapef  15446  logleb  15543  logrpap0b  15544  cxplt  15584  cxple  15585  rpcxple2  15586  rpcxplt2  15587  cxplt3  15588  cxple3  15589  apcxp2  15607  logbleb  15629  logblt  15630  lgsdilem  15700  lgsne0  15711  lgsquadlem1  15750  lgsquadlem2  15751  m1lgs  15758  2lgslem1a  15761  2lgs  15777  ausgrusgrben  15960  iooref1o  16361