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

Theorem iba 531
 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 475 . 2 (𝜑 → (𝜓 → (𝜓𝜑)))
2 simpl 486 . 2 ((𝜓𝜑) → 𝜓)
31, 2impbid1 228 1 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  ibar  532  biantru  533  biantrud  535  ancrb  551  pm5.54  1015  dedlem0a  1039  unineq  4204  fvopab6  6778  fressnfv  6899  tpostpos  7897  odi  8190  nnmword  8244  ltmpi  10317  maducoeval2  21252  mdbr2  30086  mdsl2i  30112  poimirlem26  35099  poimirlem27  35100  itg2addnclem  35124  itg2addnclem3  35126  prjspeclsp  39621  rmydioph  39970  expdioph  39979  dmafv2rnb  43800
 Copyright terms: Public domain W3C validator