Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 . Its associated inference is mpi . (Contributed by NM, 29-Dec-1992) (Proof shortened by Wolf Lammen, 4-Aug-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | com12.1 | |- ( ph -> ( ps -> ch ) ) |
|
| Assertion | com12 | |- ( ps -> ( ph -> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | com12.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | id | |- ( ps -> ps ) |
|
| 3 | 2 1 | syl5com | |- ( ps -> ( ph -> ch ) ) |