![]() |
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 107 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-ia3 107 |
This theorem is referenced by: pm3.21 262 pm3.2i 270 pm3.43i 271 ibar 299 jca 304 jcad 305 ancl 316 imnan 680 pm3.2an3 1161 19.29 1600 r19.26 2561 r19.29 2572 difrab 3355 dmcosseq 4818 lediv2a 8677 ssfzo12 10032 r19.29uz 10796 |
Copyright terms: Public domain | W3C validator |