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

Theorem iba 524
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 464 . 2 (𝜑 → (𝜓 → (𝜓𝜑)))
2 simpl 473 . 2 ((𝜓𝜑) → 𝜓)
31, 2impbid1 215 1 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  biantru  526  biantrud  528  ancrb  572  pm5.54  942  rbaibr  945  rbaibd  948  dedlem0a  999  unineq  3858  fvopab6  6267  fressnfv  6382  tpostpos  7318  odi  7605  nnmword  7659  ltmpi  9671  maducoeval2  20360  hausdiag  21353  mdbr2  28995  mdsl2i  29021  poimirlem26  33053  poimirlem27  33054  itg2addnclem  33079  itg2addnclem3  33081  rmydioph  37047  expdioph  37056
  Copyright terms: Public domain W3C validator