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

Theorem iba 528
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 472 . 2 (𝜑 → (𝜓 → (𝜓𝜑)))
2 simpl 483 . 2 ((𝜓𝜑) → 𝜓)
31, 2impbid1 226 1 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  ibar  529  biantru  530  biantrud  532  ancrb  548  pm5.54  1011  dedlem0a  1035  unineq  4253  fvopab6  6794  fressnfv  6915  tpostpos  7903  odi  8195  nnmword  8249  ltmpi  10315  maducoeval2  21179  mdbr2  30001  mdsl2i  30027  poimirlem26  34800  poimirlem27  34801  itg2addnclem  34825  itg2addnclem3  34827  prjspeclsp  39142  rmydioph  39491  expdioph  39500  dmafv2rnb  43309
  Copyright terms: Public domain W3C validator