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 2061 euexex 2062 mob 2839 issref 4891 relresfld 5038 poxp 6097 nndi 6350 nnmass 6351 pr2ne 7016 distrlem5prl 7362 distrlem5pru 7363 lbreu 8671 flqeqceilz 10059 divconjdvds 11474 algcvga 11659 algfx 11660 fiinopn 12098 |
Copyright terms: Public domain | W3C validator |