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

Theorem iba 519
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 459 . 2 (𝜑 → (𝜓 → (𝜓𝜑)))
2 simpl 470 . 2 ((𝜓𝜑) → 𝜓)
31, 2impbid1 216 1 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  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 198  df-an 385
This theorem is referenced by:  biantru  521  biantrud  523  rbaibr  529  rbaibd  532  ancrb  539  pm5.54  1032  dedlem0a  1057  unineq  4079  fvopab6  6532  fressnfv  6651  tpostpos  7607  odi  7896  nnmword  7950  ltmpi  10011  maducoeval2  20657  hausdiag  21662  mdbr2  29483  mdsl2i  29509  poimirlem26  33748  poimirlem27  33749  itg2addnclem  33773  itg2addnclem3  33775  rmydioph  38082  expdioph  38091  dmafv2rnb  41818
  Copyright terms: Public domain W3C validator