MPE Home 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 215 1 (𝜑 → (𝜓 ↔ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  biantru  525  biantrud  527  ancrb  572  pm5.54  963  rbaibr  966  rbaibd  969  dedlem0a  1012  unineq  3910  fvopab6  6350  fressnfv  6467  tpostpos  7417  odi  7704  nnmword  7758  ltmpi  9764  maducoeval2  20494  hausdiag  21496  mdbr2  29283  mdsl2i  29309  poimirlem26  33565  poimirlem27  33566  itg2addnclem  33591  itg2addnclem3  33593  rmydioph  37898  expdioph  37907
  Copyright terms: Public domain W3C validator