|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > iba | Structured version Visualization version GIF version | ||
| Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) | 
| Ref | Expression | 
|---|---|
| iba | ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | pm3.21 471 | . 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) | |
| 2 | simpl 482 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓) | |
| 3 | 1, 2 | impbid1 225 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: ibar 528 biantru 529 biantrud 531 ancrb 547 pm5.54 1019 dedlem0a 1043 r19.29r 3115 unineq 4287 fvopab6 7049 fressnfv 7179 tpostpos 8272 odi 8618 nnmword 8672 ltmpi 10945 maducoeval2 22647 mdbr2 32316 mdsl2i 32342 poimirlem26 37654 poimirlem27 37655 itg2addnclem 37679 itg2addnclem3 37681 prjspeclsp 42627 rmydioph 43031 expdioph 43040 dmafv2rnb 47246 | 
| Copyright terms: Public domain | W3C validator |