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

Theorem imbi1d 231
Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
imbi1d  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprd 158 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 75 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 144 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 75 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 129 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( 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:  imbi12d  234  imbi1  236  imim21b  253  pm5.33  609  imordc  897  drsb1  1799  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  cbvabw  2300  raleqf  2668  rspceaimv  2849  alexeq  2863  mo2icl  2916  sbc19.21g  3031  csbcow  3068  csbiebg  3099  ralss  3221  ifmdc  3573  ssuni  3829  intmin4  3870  ssexg  4139  pocl  4300  frforeq1  4340  frforeq2  4342  frind  4349  ontr2exmid  4521  elirr  4537  en2lp  4550  tfisi  4583  vtoclr  4671  sosng  4696  fun11  5279  funimass4  5562  dff13  5763  f1mpt  5766  isopolem  5817  oprabid  5901  caovcan  6033  caoftrn  6102  dfsmo2  6282  tfr1onlemsucfn  6335  tfr1onlemsucaccv  6336  tfr1onlembxssdm  6338  tfr1onlembfn  6339  tfr1onlemres  6344  tfrcllemsucfn  6348  tfrcllemsucaccv  6349  tfrcllembxssdm  6351  tfrcllembfn  6352  tfrcllemres  6357  tfrcl  6359  qliftfun  6611  ecoptocl  6616  ecopovtrn  6626  ecopovtrng  6629  dom2lem  6766  ssfiexmid  6870  domfiexmid  6872  findcard  6882  findcard2  6883  findcard2s  6884  fiintim  6922  supmoti  6986  eqsupti  6989  suplubti  6993  supisoex  7002  isomnimap  7129  ismkvmap  7146  iswomnimap  7158  tapeq1  7242  ltsonq  7385  prarloclem3  7484  suplocexpr  7712  lttrsr  7749  mulextsr1  7768  suplocsrlem  7795  axpre-lttrn  7871  axpre-mulext  7875  axcaucvglemres  7886  axpre-suploclemres  7888  axpre-suploc  7889  prime  9338  raluz  9564  indstr  9579  supinfneg  9581  infsupneg  9582  fz1sbc  10079  exbtwnzlemshrink  10232  rebtwn2zlemshrink  10237  apexp1  10679  zfz1iso  10802  caucvgre  10971  maxleast  11203  rexanre  11210  rexico  11211  minmax  11219  xrminmax  11254  addcn2  11299  mulcn2  11301  cn1lem  11303  zsupcllemstep  11926  zsupcllemex  11927  zsupssdc  11935  bezoutlemmain  11979  dfgcd2  11995  exprmfct  12118  prmdvdsexpr  12130  sqrt2irr  12142  pw2dvdslemn  12145  prmpwdvds  12333  infpn2  12437  istopg  13161  lmbr  13377  metcnp  13676  addcncntoplem  13715  2sqlem6  14120  2sqlem8  14123  2sqlem10  14125  bj-rspgt  14191  bdssexg  14309  strcollnft  14389  sscoll2  14393
  Copyright terms: Public domain W3C validator