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  1397  xordidc  1399  19.32dc  1677  r19.32vdc  2624  opbrop  4699  fvopab3g  5581  respreima  5636  fmptco  5674  cocan1  5778  cocan2  5779  brtposg  6245  nnmword  6509  swoer  6553  erth  6569  brecop  6615  ecopovsymg  6624  xpdom2  6821  ctssdccl  7100  omniwomnimkv  7155  nninfwlporlemd  7160  pitric  7295  ltexpi  7311  ltapig  7312  ltmpig  7313  ltanqg  7374  ltmnqg  7375  enq0breq  7410  genpassl  7498  genpassu  7499  1idprl  7564  1idpru  7565  caucvgprlemcanl  7618  ltasrg  7744  prsrlt  7761  caucvgsrlemoffcau  7772  ltpsrprg  7777  map2psrprg  7779  axpre-ltadd  7860  subsub23  8136  leadd1  8361  lemul1  8524  reapmul1lem  8525  reapmul1  8526  reapadd1  8527  apsym  8537  apadd1  8539  apti  8553  apcon4bid  8555  lediv1  8797  lt2mul2div  8807  lerec  8812  ltdiv2  8815  lediv2  8819  le2msq  8829  avgle1  9130  avgle2  9131  nn01to3  9588  qapne  9610  cnref1o  9621  xleneg  9806  xsubge0  9850  xleaddadd  9856  iooneg  9957  iccneg  9958  iccshftr  9963  iccshftl  9965  iccdil  9967  icccntr  9969  fzsplit2  10018  fzaddel  10027  fzrev  10052  elfzo  10117  fzon  10134  elfzom1b  10197  ioo0  10228  ico0  10230  ioc0  10231  flqlt  10251  negqmod0  10299  frec2uzled  10397  expeq0  10519  nn0leexp2  10657  nn0opthlem1d  10666  leisorel  10783  cjreb  10841  ltmininf  11209  minclpr  11211  xrmaxlesup  11233  xrltmininf  11244  xrminltinf  11246  tanaddaplem  11712  nndivdvds  11769  moddvds  11772  modmulconst  11796  oddm1even  11845  ltoddhalfle  11863  dvdssq  11997  phiprmpw  12187  eulerthlemh  12196  odzdvds  12210  pc2dvds  12294  1arith  12330  ablsubsub23  12924  issrgid  12957  isringid  13001  cnrest2  13287  cnptoprest  13290  cnptoprest2  13291  lmss  13297  lmff  13300  txlm  13330  ismet2  13405  blres  13485  xmetec  13488  bdbl  13554  metrest  13557  cnbl0  13585  cnblcld  13586  reopnap  13589  bl2ioo  13593  limcdifap  13682  efle  13748  reapef  13750  logleb  13847  logrpap0b  13848  cxplt  13887  cxple  13888  rpcxple2  13889  rpcxplt2  13890  cxplt3  13891  cxple3  13892  apcxp2  13909  logbleb  13930  logblt  13931  lgsdilem  13979  lgsne0  13990  iooref1o  14323