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 1171 | . . 3 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
3 | 2 | 3adant1r 1194 | . 2 ⊢ (((𝜒 ∧ 𝜏) ∧ 𝜓 ∧ 𝜑) → 𝜃) |
4 | 3 | 3com13 1171 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 947 |
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 949 |
This theorem is referenced by: addassnqg 7158 mulassnqg 7160 prarloc 7279 ltpopr 7371 ltexprlemfl 7385 ltexprlemfu 7387 addasssrg 7532 axaddass 7648 apmul1 8516 ltmul2 8582 lemul2 8583 dvdscmulr 11449 dvdsmulcr 11450 modremain 11553 ndvdsadd 11555 rpexp12i 11760 xblcntrps 12509 xblcntr 12510 |
Copyright terms: Public domain | W3C validator |