![]() |
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 106 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-ia3 106 |
This theorem is referenced by: pm3.21 260 pm3.2i 266 pm3.43i 267 ibar 295 jca 300 jcad 301 ancl 311 imnan 657 pm3.2an3 1118 19.29 1552 r19.26 2490 r19.29 2499 difrab 3254 dmcosseq 4651 lediv2a 8092 ssfzo12 9362 r19.29uz 10079 |
Copyright terms: Public domain | W3C validator |