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

Theorem iba 523
 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 463 . 2 (𝜑 → (𝜓 → (𝜓𝜑)))
2 simpl 472 . 2 ((𝜓𝜑) → 𝜓)
31, 2impbid1 214 1 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  biantru  525  biantrud  527  ancrb  571  pm5.54  941  rbaibr  944  rbaibd  947  dedlem0a  991  unineq  3836  fvopab6  6218  fressnfv  6332  tpostpos  7259  odi  7546  nnmword  7600  ltmpi  9605  maducoeval2  20265  hausdiag  21258  mdbr2  28539  mdsl2i  28565  poimirlem26  32605  poimirlem27  32606  itg2addnclem  32631  itg2addnclem3  32633  rmydioph  36599  expdioph  36608
 Copyright terms: Public domain W3C validator