Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > com3r | GIF version |
Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.) |
Ref | Expression |
---|---|
com3.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
com3r | ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com3.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
2 | 1 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
3 | 2 | com12 30 | 1 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃))) |
Colors of variables: wff set 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: com13 80 com3l 81 com14 88 expd 256 moexexdc 2090 euexex 2091 mob 2894 issref 4968 relresfld 5115 poxp 6179 nndi 6433 nnmass 6434 pr2ne 7127 distrlem5prl 7506 distrlem5pru 7507 lbreu 8816 flqeqceilz 10217 divconjdvds 11741 algcvga 11928 algfx 11929 fiinopn 12413 |
Copyright terms: Public domain | W3C validator |