![]() |
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 3114 unineq 4294 fvopab6 7050 fressnfv 7180 tpostpos 8270 odi 8616 nnmword 8670 ltmpi 10942 maducoeval2 22662 mdbr2 32325 mdsl2i 32351 poimirlem26 37633 poimirlem27 37634 itg2addnclem 37658 itg2addnclem3 37660 prjspeclsp 42599 rmydioph 43003 expdioph 43012 dmafv2rnb 47179 |
Copyright terms: Public domain | W3C validator |