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 1197 rspct 2782 po2nr 4231 funssres 5165 f1ocnv2d 5974 tfrlem9 6216 nnmass 6383 nnmordi 6412 genpcdl 7327 genpcuu 7328 mulnqprl 7376 mulnqpru 7377 distrlem1prl 7390 distrlem1pru 7391 divgt0 8630 divge0 8631 uzind2 9163 facdiv 10484 dvdsabseq 11545 divgcdcoprm0 11782 |
Copyright terms: Public domain | W3C validator |