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

Theorem bitr3d 190
Description: Deduction form of bitr3i 186. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitr3d.2  |-  ( ph  ->  ( ps  <->  th )
)
Assertion
Ref Expression
bitr3d  |-  ( ph  ->  ( ch  <->  th )
)

Proof of Theorem bitr3d
StepHypRef Expression
1 bitr3d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21bicomd 141 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 188 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
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:  3bitrrd  215  3bitr3d  218  3bitr3rd  219  pm5.16  828  biassdc  1395  pm5.24dc  1398  anxordi  1400  sbequ12a  1773  drex1  1798  sbcomxyyz  1972  sb9v  1978  csbiebt  3096  prsspwg  3750  bnd2  4170  copsex2t  4242  copsex2g  4243  fnssresb  5324  fcnvres  5395  foelcdmi  5564  dmfco  5580  funimass5  5629  fmptco  5678  cbvfo  5780  cbvexfo  5781  isocnv  5806  isoini  5813  isoselem  5815  riota2df  5845  ovmpodxf  5994  caovcanrd  6032  fidcenumlemrks  6946  ordiso2  7028  ltpiord  7306  dfplpq2  7341  dfmpq2  7342  enqeceq  7346  enq0eceq  7424  enreceq  7723  ltpsrprg  7790  mappsrprg  7791  cnegexlem3  8121  subeq0  8170  negcon1  8196  subexsub  8316  subeqrev  8320  lesub  8385  ltsub13  8387  subge0  8419  div11ap  8643  divmuleqap  8660  ltmuldiv2  8818  lemuldiv2  8825  nn1suc  8924  addltmul  9141  elnnnn0  9205  znn0sub  9304  prime  9338  indstr  9579  qapne  9625  qlttri2  9627  fz1n  10027  fzrev3  10070  fzonlt0  10150  divfl0  10279  modqsubdir  10376  fzfig  10413  sqrt11  11029  sqrtsq2  11033  absdiflt  11082  absdifle  11083  nnabscl  11090  minclpr  11226  xrnegiso  11251  xrnegcon1d  11253  clim2  11272  climshft2  11295  sumrbdc  11368  prodrbdclem2  11562  fprodssdc  11579  sinbnd  11741  cosbnd  11742  dvdscmulr  11808  dvdsmulcr  11809  oddm1even  11860  qredeq  12076  cncongr2  12084  isprm3  12098  prmrp  12125  sqrt2irr  12142  crth  12204  pcdvdsb  12299  ssnnctlemct  12427  grpid  12799  grpidrcan  12821  grpidlcan  12822  grplmulf1o  12830  abladdsub4  12941  eltg3  13217  eltop  13229  eltop2  13230  eltop3  13231  lmbrf  13375  cncnpi  13388  txcn  13435  hmeoimaf1o  13474  ismet2  13514  xmseq0  13628  lgsne0  14099  2sqlem7  14117
  Copyright terms: Public domain W3C validator