![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3adant3r | GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3adant1l.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant3r | ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adant1l.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
2 | 1 | 3com13 1208 | . . 3 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
3 | 2 | 3adant1r 1231 | . 2 ⊢ (((𝜒 ∧ 𝜏) ∧ 𝜓 ∧ 𝜑) → 𝜃) |
4 | 3 | 3com13 1208 | 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: addassnqg 7384 mulassnqg 7386 prarloc 7505 ltpopr 7597 ltexprlemfl 7611 ltexprlemfu 7613 addasssrg 7758 axaddass 7874 apmul1 8748 ltmul2 8816 lemul2 8817 dvdscmulr 11830 dvdsmulcr 11831 modremain 11937 ndvdsadd 11939 rpexp12i 12158 xblcntrps 14053 xblcntr 14054 |
Copyright terms: Public domain | W3C validator |