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 1340 merco2 1728 onint 7498 oalimcl 8176 oeordsuc 8210 fisup2g 8921 fiinf2g 8953 zorn2lem7 9913 inar1 10186 rpnnen1lem5 12370 expnbnd 13583 facwordi 13639 fi1uzind 13845 brfi1indALT 13848 unbenlem 16234 fiinopn 21439 cmpsublem 21937 dvcnvrelem1 24543 axcontlem4 26681 axcont 26690 spansncol 29273 atcvat4i 30102 sumdmdlem 30123 nocvxminlem 33145 broutsideof2 33481 relowlpssretop 34528 cvrat4 36461 pm2.43cbi 40732 |
Copyright terms: Public domain | W3C validator |