Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ad2ant2rl | GIF version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.) |
Ref | Expression |
---|---|
ad2ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad2ant2rl | ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantrl 469 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantlr 468 | 1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
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 is referenced by: fvtp1g 5596 fcof1o 5658 infnfi 6757 addcomnqg 7157 addassnqg 7158 nqtri3or 7172 ltexnqq 7184 nqnq0pi 7214 nqpnq0nq 7229 nqnq0a 7230 addassnq0lemcl 7237 ltaddpr 7373 ltexprlemloc 7383 addcanprlemu 7391 recexprlem1ssu 7410 aptiprleml 7415 mulcomsrg 7533 mulasssrg 7534 distrsrg 7535 aptisr 7555 mulcnsr 7611 cnegex 7908 muladd 8114 lemul12b 8587 qaddcl 9395 iooshf 9703 elfzomelpfzo 9976 expnegzap 10295 setscom 11926 cnpnei 12315 |
Copyright terms: Public domain | W3C validator |