Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > com45 | Structured version Visualization version Unicode version |
Description: Commutation of antecedents. Swap 4th and 5th. Deduction associated with com34 91. Double deduction associated with com23 86. Triple deduction associated with com12 32. (Contributed by Jeff Hankins, 28-Jun-2009.) |
Ref | Expression |
---|---|
com5.1 |
Ref | Expression |
---|---|
com45 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com5.1 | . 2 | |
2 | pm2.04 90 | . 2 | |
3 | 1, 2 | syl8 76 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: com35 98 com25 99 com5l 100 ad5ant13 1301 ad5ant14 1302 ad5ant15 1303 ad5ant23 1304 ad5ant24 1305 ad5ant25 1306 ad5ant235 1309 ad5ant123 1310 ad5ant124 1311 ad5ant134 1313 ad5ant135 1314 lcmfdvdsb 15356 prmgaplem6 15760 islmhm2 19038 dfon2lem8 31695 |
Copyright terms: Public domain | W3C validator |