![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm3.2 | GIF version |
Description: Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) (Proof shortened by Jia Ming, 17-Nov-2020.) |
Ref | Expression |
---|---|
pm3.2 | ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ia3 108 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-ia3 108 |
This theorem is referenced by: pm3.21 264 pm3.2i 272 pm3.43i 273 ibar 301 jca 306 jcad 307 ancl 318 imnan 691 pm3.2an3 1178 19.29 1631 r19.26 2616 r19.29 2627 difrab 3424 dmcosseq 4916 lediv2a 8882 ssfzo12 10254 r19.29uz 11033 |
Copyright terms: Public domain | W3C validator |