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  4738  fvopab3g  5630  respreima  5686  fmptco  5724  cocan1  5830  cocan2  5831  brtposg  6307  nnmword  6571  swoer  6615  erth  6633  brecop  6679  ecopovsymg  6688  xpdom2  6885  pw2f1odclem  6890  opabfi  6992  ctssdccl  7170  omniwomnimkv  7226  nninfwlporlemd  7231  pitric  7381  ltexpi  7397  ltapig  7398  ltmpig  7399  ltanqg  7460  ltmnqg  7461  enq0breq  7496  genpassl  7584  genpassu  7585  1idprl  7650  1idpru  7651  caucvgprlemcanl  7704  ltasrg  7830  prsrlt  7847  caucvgsrlemoffcau  7858  ltpsrprg  7863  map2psrprg  7865  axpre-ltadd  7946  subsub23  8224  leadd1  8449  lemul1  8612  reapmul1lem  8613  reapmul1  8614  reapadd1  8615  apsym  8625  apadd1  8627  apti  8641  apcon4bid  8643  lediv1  8888  lt2mul2div  8898  lerec  8903  ltdiv2  8906  lediv2  8910  le2msq  8920  avgle1  9223  avgle2  9224  nn01to3  9682  qapne  9704  cnref1o  9716  xleneg  9903  xsubge0  9947  xleaddadd  9953  iooneg  10054  iccneg  10055  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  fzsplit2  10116  fzaddel  10125  fzrev  10150  elfzo  10215  nelfzo  10218  fzon  10233  elfzom1b  10296  ioo0  10328  ico0  10330  ioc0  10331  flqlt  10352  negqmod0  10402  frec2uzled  10500  expeq0  10641  nn0leexp2  10781  nn0opthlem1d  10791  leisorel  10908  cjreb  11010  ltmininf  11378  minclpr  11380  xrmaxlesup  11402  xrltmininf  11413  xrminltinf  11415  tanaddaplem  11881  nndivdvds  11939  moddvds  11942  modmulconst  11966  oddm1even  12016  ltoddhalfle  12034  dvdssq  12168  phiprmpw  12360  eulerthlemh  12369  odzdvds  12383  pc2dvds  12468  1arith  12505  issubg3  13262  eqgid  13296  resghm2b  13332  conjghm  13346  conjnmzb  13350  ablsubsub23  13395  issrgid  13477  isringid  13521  opprsubgg  13580  opprunitd  13606  crngunit  13607  unitpropdg  13644  issubrng  13695  opprsubrngg  13707  lsslss  13877  lsspropdg  13927  rspsn  14030  znidom  14145  cnrest2  14404  cnptoprest  14407  cnptoprest2  14408  lmss  14414  lmff  14417  txlm  14447  ismet2  14522  blres  14602  xmetec  14605  bdbl  14671  metrest  14674  cnbl0  14702  cnblcld  14703  reopnap  14706  bl2ioo  14710  limcdifap  14816  efle  14911  reapef  14913  logleb  15010  logrpap0b  15011  cxplt  15050  cxple  15051  rpcxple2  15052  rpcxplt2  15053  cxplt3  15054  cxple3  15055  apcxp2  15072  logbleb  15093  logblt  15094  lgsdilem  15143  lgsne0  15154  lgsquadlem1  15191  m1lgs  15192  iooref1o  15524