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 2103 euexex 2104 mob 2912 issref 4993 relresfld 5140 poxp 6211 nndi 6465 nnmass 6466 pr2ne 7169 distrlem5prl 7548 distrlem5pru 7549 lbreu 8861 flqeqceilz 10274 divconjdvds 11809 algcvga 12005 algfx 12006 fiinopn 12796 |
Copyright terms: Public domain | W3C validator |