MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iba Structured version   Visualization version   GIF version

Theorem iba 527
Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.)
Assertion
Ref Expression
iba (𝜑 → (𝜓 ↔ (𝜓𝜑)))

Proof of Theorem iba
StepHypRef Expression
1 pm3.21 471 . 2 (𝜑 → (𝜓 → (𝜓𝜑)))
2 simpl 482 . 2 ((𝜓𝜑) → 𝜓)
31, 2impbid1 225 1 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 207  df-an 396
This theorem is referenced by:  ibar  528  biantru  529  biantrud  531  ancrb  547  pm5.54  1019  dedlem0a  1043  r19.29r  3114  unineq  4294  fvopab6  7050  fressnfv  7180  tpostpos  8270  odi  8616  nnmword  8670  ltmpi  10942  maducoeval2  22662  mdbr2  32325  mdsl2i  32351  poimirlem26  37633  poimirlem27  37634  itg2addnclem  37658  itg2addnclem3  37660  prjspeclsp  42599  rmydioph  43003  expdioph  43012  dmafv2rnb  47179
  Copyright terms: Public domain W3C validator