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 469 | . 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
3 | 2 | 3adantl2 1143 | 1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: acexmid 5835 ordiso2 6991 addlocpr 7468 distrlem1prl 7514 distrlem1pru 7515 ltsopr 7528 addcanprlemu 7547 fzo1fzo0n0 10108 prodfap0 11472 prodfrecap 11473 muldvds2 11743 dvds2add 11751 dvds2sub 11752 dvdstr 11754 cnpnei 12760 upxp 12813 |
Copyright terms: Public domain | W3C validator |