![]() |
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 2084 euexex 2085 mob 2870 issref 4929 relresfld 5076 poxp 6137 nndi 6390 nnmass 6391 pr2ne 7065 distrlem5prl 7418 distrlem5pru 7419 lbreu 8727 flqeqceilz 10122 divconjdvds 11583 algcvga 11768 algfx 11769 fiinopn 12210 |
Copyright terms: Public domain | W3C validator |