![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3ad2antl1 | GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
Ref | Expression |
---|---|
3ad2antl.1 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3ad2antl1 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2antl.1 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
2 | 1 | adantlr 477 | . 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
3 | 2 | 3adantl2 1154 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: acexmid 5867 ordiso2 7027 addlocpr 7513 distrlem1prl 7559 distrlem1pru 7560 ltsopr 7573 addcanprlemu 7592 fzo1fzo0n0 10156 prodfap0 11524 prodfrecap 11525 muldvds2 11795 dvds2add 11803 dvds2sub 11804 dvdstr 11806 mulgnnsubcl 12871 mulgpropdg 12900 ringidss 13025 cnpnei 13352 upxp 13405 lgsval4lem 14045 |
Copyright terms: Public domain | W3C validator |