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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpdfbidc  998  dfbi3dc  1446  xordidc  1448  19.32dc  1731  r19.32vdc  2700  opbrop  4856  fvopab3g  5781  respreima  5839  fmptco  5877  cocan1  5996  cocan2  5997  suppimacnvfn  6490  brtposg  6529  nnmword  6795  swoer  6839  erth  6857  brecop  6903  ecopovsymg  6912  xpdom2  7133  pw2f1odclem  7138  opabfi  7251  ctssdccl  7457  omniwomnimkv  7513  nninfwlporlemd  7518  pitric  7694  ltexpi  7710  ltapig  7711  ltmpig  7712  ltanqg  7773  ltmnqg  7774  enq0breq  7809  genpassl  7897  genpassu  7898  1idprl  7963  1idpru  7964  caucvgprlemcanl  8017  ltasrg  8143  prsrlt  8160  caucvgsrlemoffcau  8171  ltpsrprg  8176  map2psrprg  8178  axpre-ltadd  8259  subsub23  8538  leadd1  8765  lemul1  8929  reapmul1lem  8930  reapmul1  8931  reapadd1  8932  apsym  8942  apadd1  8944  apti  8958  apcon4bid  8960  lediv1  9207  lt2mul2div  9217  lerec  9222  ltdiv2  9225  lediv2  9229  le2msq  9239  ofsubeq0  9300  avgle1  9557  avgle2  9558  nn01to3  10033  qapne  10055  cnref1o  10068  xleneg  10256  xsubge0  10300  xleaddadd  10306  iooneg  10407  iccneg  10408  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  fzsplit2  10472  fzaddel  10482  fzrev  10508  elfzo  10573  nelfzo  10576  fzon  10591  elfzom1b  10664  ioo0  10711  ico0  10713  ioc0  10714  flqlt  10738  negqmod0  10789  frec2uzled  10887  expeq0  11028  nn0leexp2  11170  nn0opthlem1d  11180  leisorel  11311  cjreb  11653  ltmininf  12025  minclpr  12027  xrmaxlesup  12050  xrltmininf  12061  xrminltinf  12063  tanaddaplem  12530  nndivdvds  12588  moddvds  12591  modmulconst  12615  oddm1even  12667  ltoddhalfle  12685  bitsp1  12743  dvdssq  12833  phiprmpw  13029  eulerthlemh  13038  odzdvds  13053  pc2dvds  13138  1arith  13175  issubg3  14054  eqgid  14088  resghm2b  14124  conjghm  14138  conjnmzb  14142  resscntz  14166  cntzrec  14169  ablsubsub23  14219  issrgid  14392  isringid  14437  opprsubgg  14499  opprunitd  14526  crngunit  14527  unitpropdg  14564  issubrng  14616  opprsubrngg  14628  opprdrng  14729  lsslss  14827  lsspropdg  14877  rspsn  14980  znidom  15101  psrbagconf1o  15174  gsumbagdiaglem  15175  cnrest2  15462  cnptoprest  15465  cnptoprest2  15466  lmss  15472  lmff  15475  txlm  15505  ismet2  15580  blres  15660  xmetec  15663  bdbl  15729  metrest  15732  cnbl0  15760  cnblcld  15761  reopnap  15772  bl2ioo  15776  limcdifap  15888  efle  16002  reapef  16004  logleb  16105  logrpap0b  16106  logdivle  16125  cxplt  16151  cxple  16152  rpcxple2  16153  rpcxplt2  16154  cxplt3  16155  cxple3  16156  apcxp2  16174  logbleb  16197  logblt  16198  lgsdilem  16351  lgsne0  16362  lgsquadlem1  16401  lgsquadlem2  16402  m1lgs  16409  2lgslem1a  16412  2lgs  16428  ausgrusgrben  16614  uspgr2wlkeq  16811  isclwwlknx  16862  eupth2lem3lem6fi  16917  iooref1o  17289