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 1208 rspct 2818 po2nr 4281 funssres 5224 f1ocnv2d 6036 tfrlem9 6278 nnmass 6446 nnmordi 6475 genpcdl 7451 genpcuu 7452 mulnqprl 7500 mulnqpru 7501 distrlem1prl 7514 distrlem1pru 7515 divgt0 8758 divge0 8759 uzind2 9294 facdiv 10640 dvdsabseq 11770 divgcdcoprm0 12012 |
Copyright terms: Public domain | W3C validator |