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 77 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
3 | 2 | com12 30 | 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: com13 79 com3l 80 com14 87 expd 254 moexexdc 2025 euexex 2026 mob 2774 issref 4727 relresfld 4867 poxp 5873 nndi 6088 nnmass 6089 pr2ne 6461 distrlem5prl 6776 distrlem5pru 6777 lbreu 8023 flqeqceilz 9320 divconjdvds 10249 ialgcvga 10433 ialgfx 10434 |
Copyright terms: Public domain | W3C validator |