ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1d GIF 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 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4 (𝜑 → (𝜓𝜒))
21biimprd 158 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 75 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 144 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 75 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 129 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
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  4299  frforeq1  4339  frforeq2  4341  frind  4348  ontr2exmid  4520  elirr  4536  en2lp  4549  tfisi  4582  vtoclr  4670  sosng  4695  fun11  5278  funimass4  5561  dff13  5762  f1mpt  5765  isopolem  5816  oprabid  5900  caovcan  6032  caoftrn  6101  dfsmo2  6281  tfr1onlemsucfn  6334  tfr1onlemsucaccv  6335  tfr1onlembxssdm  6337  tfr1onlembfn  6338  tfr1onlemres  6343  tfrcllemsucfn  6347  tfrcllemsucaccv  6348  tfrcllembxssdm  6350  tfrcllembfn  6351  tfrcllemres  6356  tfrcl  6358  qliftfun  6610  ecoptocl  6615  ecopovtrn  6625  ecopovtrng  6628  dom2lem  6765  ssfiexmid  6869  domfiexmid  6871  findcard  6881  findcard2  6882  findcard2s  6883  fiintim  6921  supmoti  6985  eqsupti  6988  suplubti  6992  supisoex  7001  isomnimap  7128  ismkvmap  7145  iswomnimap  7157  ltsonq  7375  prarloclem3  7474  suplocexpr  7702  lttrsr  7739  mulextsr1  7758  suplocsrlem  7785  axpre-lttrn  7861  axpre-mulext  7865  axcaucvglemres  7876  axpre-suploclemres  7878  axpre-suploc  7879  prime  9328  raluz  9554  indstr  9569  supinfneg  9571  infsupneg  9572  fz1sbc  10069  exbtwnzlemshrink  10222  rebtwn2zlemshrink  10227  apexp1  10669  zfz1iso  10792  caucvgre  10961  maxleast  11193  rexanre  11200  rexico  11201  minmax  11209  xrminmax  11244  addcn2  11289  mulcn2  11291  cn1lem  11293  zsupcllemstep  11916  zsupcllemex  11917  zsupssdc  11925  bezoutlemmain  11969  dfgcd2  11985  exprmfct  12108  prmdvdsexpr  12120  sqrt2irr  12132  pw2dvdslemn  12135  prmpwdvds  12323  infpn2  12427  istopg  13130  lmbr  13346  metcnp  13645  addcncntoplem  13684  2sqlem6  14089  2sqlem8  14092  2sqlem10  14094  bj-rspgt  14160  bdssexg  14278  strcollnft  14358  sscoll2  14362
  Copyright terms: Public domain W3C validator