Description: Combine antecedents into a single biconditional. This inference, reminiscent of ja , is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im and pm5.21im ). (Contributed by Wolf Lammen, 13-May-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bija.1 | |- ( ph -> ( ps -> ch ) ) |
|
| bija.2 | |- ( -. ph -> ( -. ps -> ch ) ) |
||
| Assertion | bija | |- ( ( ph <-> ps ) -> ch ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bija.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | bija.2 | |- ( -. ph -> ( -. ps -> ch ) ) |
|
| 3 | biimpr | |- ( ( ph <-> ps ) -> ( ps -> ph ) ) |
|
| 4 | 3 1 | syli | |- ( ( ph <-> ps ) -> ( ps -> ch ) ) |
| 5 | biimp | |- ( ( ph <-> ps ) -> ( ph -> ps ) ) |
|
| 6 | 5 | con3d | |- ( ( ph <-> ps ) -> ( -. ps -> -. ph ) ) |
| 7 | 6 2 | syli | |- ( ( ph <-> ps ) -> ( -. ps -> ch ) ) |
| 8 | 4 7 | pm2.61d | |- ( ( ph <-> ps ) -> ch ) |