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

Theorem 3bitr4d 219
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 190 . 2  |-  ( ph  ->  ( ps  <->  ta )
)
51, 4bitrd 187 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  dfbi3dc  1358  xordidc  1360  19.32dc  1640  r19.32vdc  2555  opbrop  4586  fvopab3g  5460  respreima  5514  fmptco  5552  cocan1  5654  cocan2  5655  brtposg  6117  nnmword  6380  swoer  6423  erth  6439  brecop  6485  ecopovsymg  6494  xpdom2  6691  ctssdccl  6962  pitric  7093  ltexpi  7109  ltapig  7110  ltmpig  7111  ltanqg  7172  ltmnqg  7173  enq0breq  7208  genpassl  7296  genpassu  7297  1idprl  7362  1idpru  7363  caucvgprlemcanl  7416  ltasrg  7542  prsrlt  7559  caucvgsrlemoffcau  7570  ltpsrprg  7575  map2psrprg  7577  axpre-ltadd  7658  subsub23  7931  leadd1  8156  lemul1  8318  reapmul1lem  8319  reapmul1  8320  reapadd1  8321  apsym  8331  apadd1  8333  apti  8347  apcon4bid  8349  lediv1  8587  lt2mul2div  8597  lerec  8602  ltdiv2  8605  lediv2  8609  le2msq  8619  avgle1  8914  avgle2  8915  nn01to3  9361  qapne  9383  cnref1o  9392  xleneg  9571  xsubge0  9615  xleaddadd  9621  iooneg  9722  iccneg  9723  iccshftr  9728  iccshftl  9730  iccdil  9732  icccntr  9734  fzsplit2  9781  fzaddel  9790  fzrev  9815  elfzo  9877  fzon  9894  elfzom1b  9957  ioo0  9988  ico0  9990  ioc0  9991  flqlt  10007  negqmod0  10055  frec2uzled  10153  expeq0  10275  nn0opthlem1d  10417  leisorel  10531  cjreb  10589  ltmininf  10957  minclpr  10959  xrmaxlesup  10979  xrltmininf  10990  xrminltinf  10992  tanaddaplem  11355  nndivdvds  11406  moddvds  11409  modmulconst  11432  oddm1even  11479  ltoddhalfle  11497  dvdssq  11626  phiprmpw  11804  cnrest2  12311  cnptoprest  12314  cnptoprest2  12315  lmss  12321  lmff  12324  txlm  12354  ismet2  12429  blres  12509  xmetec  12512  bdbl  12578  metrest  12581  cnbl0  12609  cnblcld  12610  reopnap  12613  bl2ioo  12617  limcdifap  12706
  Copyright terms: Public domain W3C validator