Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > com34 | GIF version |
Description: Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.) |
Ref | Expression |
---|---|
com4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
com34 | ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com4.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | pm2.04 76 | . 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏))) | |
3 | 1, 2 | syl6 29 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏)))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com4l 78 com35 84 3an1rs 1116 rspct 2649 po2nr 4046 funssres 4942 f1ocnv2d 5704 tfrlem9 5935 nnmass 6066 nnmordi 6089 genpcdl 6617 genpcuu 6618 mulnqprl 6666 mulnqpru 6667 distrlem1prl 6680 distrlem1pru 6681 divgt0 7838 divge0 7839 uzind2 8350 |
Copyright terms: Public domain | W3C validator |