![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > com34 | GIF version |
Description: Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.) |
Ref | Expression |
---|---|
com4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
com34 | ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com4.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | pm2.04 82 | . 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏))) | |
3 | 1, 2 | syl6 33 | 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: com4l 84 com35 90 3an1rs 1221 rspct 2849 po2nr 4330 funssres 5280 f1ocnv2d 6102 tfrlem9 6348 nnmass 6516 nnmordi 6545 genpcdl 7553 genpcuu 7554 mulnqprl 7602 mulnqpru 7603 distrlem1prl 7616 distrlem1pru 7617 divgt0 8864 divge0 8865 uzind2 9400 facdiv 10759 dvdsabseq 11894 divgcdcoprm0 12144 lmodvsdi 13652 |
Copyright terms: Public domain | W3C validator |