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 81 | . 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏))) | |
3 | 1, 2 | syl6 33 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏)))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com4l 83 com35 89 3an1rs 1150 rspct 2694 po2nr 4064 funssres 4962 f1ocnv2d 5724 tfrlem9 5958 nnmass 6089 nnmordi 6112 genpcdl 6709 genpcuu 6710 mulnqprl 6758 mulnqpru 6759 distrlem1prl 6772 distrlem1pru 6773 divgt0 7950 divge0 7951 uzind2 8459 facdiv 9665 dvdsabseq 10247 divgcdcoprm0 10483 |
Copyright terms: Public domain | W3C validator |