![]() |
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 7380 mulassnqg 7382 prarloc 7501 ltpopr 7593 ltexprlemfl 7607 ltexprlemfu 7609 addasssrg 7754 axaddass 7870 apmul1 8743 ltmul2 8811 lemul2 8812 dvdscmulr 11822 dvdsmulcr 11823 modremain 11928 ndvdsadd 11930 rpexp12i 12149 xblcntrps 13806 xblcntr 13807 |
Copyright terms: Public domain | W3C validator |