ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr4d Unicode version

Theorem 3bitr4d 213
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
StepHypRef Expression
1 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
2 3bitr4d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
3 3bitr4d.3 . . 3  |-  ( ph  ->  ( ta  <->  ch )
)
42, 3bitr4d 184 . 2  |-  ( ph  ->  ( ps  <->  ta )
)
51, 4bitrd 181 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  dfbi3dc  1304  xordidc  1306  19.32dc  1585  r19.32vdc  2476  r19.12sn  3464  opbrop  4447  fvopab3g  5273  respreima  5323  fmptco  5358  cocan1  5455  cocan2  5456  brtposg  5900  nnmword  6122  swoer  6165  erth  6181  brecop  6227  ecopovsymg  6236  xpdom2  6336  pitric  6477  ltexpi  6493  ltapig  6494  ltmpig  6495  ltanqg  6556  ltmnqg  6557  enq0breq  6592  genpassl  6680  genpassu  6681  1idprl  6746  1idpru  6747  caucvgprlemcanl  6800  ltasrg  6913  prsrlt  6929  caucvgsrlemoffcau  6940  axpre-ltadd  7018  subsub23  7279  leadd1  7499  lemul1  7658  reapmul1lem  7659  reapmul1  7660  reapadd1  7661  apsym  7671  apadd1  7673  apti  7687  lediv1  7910  lt2mul2div  7920  lerec  7925  ltdiv2  7928  lediv2  7932  le2msq  7942  avgle1  8222  avgle2  8223  nn01to3  8649  qapne  8671  cnref1o  8680  xleneg  8851  iooneg  8957  iccneg  8958  iccshftr  8963  iccshftl  8965  iccdil  8967  icccntr  8969  fzsplit2  9016  fzaddel  9024  fzrev  9048  elfzo  9108  fzon  9124  elfzom1b  9187  ioo0  9216  ico0  9218  ioc0  9219  flqlt  9233  negqmod0  9281  expeq0  9451  nn0opthlem1d  9588  cjreb  9694  abs00  9891  nndivdvds  10114  moddvds  10117  modmulconst  10139  oddm1even  10186  ltoddhalfle  10205
  Copyright terms: Public domain W3C validator