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

Theorem imbi1d 230
 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 157 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 75 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 143 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 75 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 128 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
 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:  imbi12d  233  imbi1  235  imim21b  251  pm5.33  599  imordc  883  drsb1  1773  ax11v2  1794  ax11v  1801  ax11ev  1802  equs5or  1804  raleqf  2627  rspceaimv  2803  alexeq  2817  mo2icl  2869  sbc19.21g  2983  csbiebg  3049  ralss  3170  ifmdc  3516  ssuni  3768  intmin4  3809  ssexg  4077  pocl  4236  frforeq1  4276  frforeq2  4278  frind  4285  ontr2exmid  4451  elirr  4467  en2lp  4480  tfisi  4512  vtoclr  4599  sosng  4624  fun11  5202  funimass4  5484  dff13  5681  f1mpt  5684  isopolem  5735  oprabid  5815  caovcan  5947  caoftrn  6019  dfsmo2  6196  tfr1onlemsucfn  6249  tfr1onlemsucaccv  6250  tfr1onlembxssdm  6252  tfr1onlembfn  6253  tfr1onlemres  6258  tfrcllemsucfn  6262  tfrcllemsucaccv  6263  tfrcllembxssdm  6265  tfrcllembfn  6266  tfrcllemres  6271  tfrcl  6273  qliftfun  6523  ecoptocl  6528  ecopovtrn  6538  ecopovtrng  6541  dom2lem  6678  ssfiexmid  6782  domfiexmid  6784  findcard  6794  findcard2  6795  findcard2s  6796  fiintim  6834  supmoti  6897  eqsupti  6900  suplubti  6904  supisoex  6913  isomnimap  7030  ismkvmap  7047  iswomnimap  7059  ltsonq  7259  prarloclem3  7358  suplocexpr  7586  lttrsr  7623  mulextsr1  7642  suplocsrlem  7669  axpre-lttrn  7745  axpre-mulext  7749  axcaucvglemres  7760  axpre-suploclemres  7762  axpre-suploc  7763  prime  9203  raluz  9429  indstr  9444  supinfneg  9446  infsupneg  9447  fz1sbc  9936  exbtwnzlemshrink  10086  rebtwn2zlemshrink  10091  apexp1  10525  zfz1iso  10645  caucvgre  10814  maxleast  11046  rexanre  11053  rexico  11054  minmax  11062  xrminmax  11095  addcn2  11140  mulcn2  11142  cn1lem  11144  zsupcllemstep  11710  zsupcllemex  11711  bezoutlemmain  11758  dfgcd2  11774  exprmfct  11890  prmdvdsexpr  11900  sqrt2irr  11912  pw2dvdslemn  11915  istopg  12241  lmbr  12457  metcnp  12756  addcncntoplem  12795  bj-rspgt  13203  bdssexg  13318  strcollnft  13398  sscoll2  13402
 Copyright terms: Public domain W3C validator