![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > com4l | Structured version Visualization version GIF version |
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Mel L. O'Cat, 15-Aug-2004.) |
Ref | Expression |
---|---|
com4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
com4l | ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | com3l 89 | . 2 ⊢ (𝜓 → (𝜒 → (𝜑 → (𝜃 → 𝜏)))) |
3 | 2 | com34 91 | 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: com4t 93 com4r 94 com14 96 com5l 100 3impd 1346 merco2 1731 onint 7787 oalimcl 8574 oeordsuc 8608 fisup2g 9483 fiinf2g 9515 zorn2lem7 10517 inar1 10790 rpnnen1lem5 12987 expnbnd 14218 facwordi 14272 fi1uzind 14482 brfi1indALT 14485 unbenlem 16868 fiinopn 22790 cmpsublem 23290 dvcnvrelem1 25937 nocvxminlem 27697 axcontlem4 28765 axcont 28774 spansncol 31365 atcvat4i 32194 sumdmdlem 32215 broutsideof2 35654 relowlpssretop 36779 cvrat4 38853 pm2.43cbi 43880 |
Copyright terms: Public domain | W3C validator |