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 478 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantlr 477 | 1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
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 is referenced by: fvtp1g 5716 fcof1o 5780 infnfi 6885 addcomnqg 7355 addassnqg 7356 nqtri3or 7370 ltexnqq 7382 nqnq0pi 7412 nqpnq0nq 7427 nqnq0a 7428 addassnq0lemcl 7435 ltaddpr 7571 ltexprlemloc 7581 addcanprlemu 7589 recexprlem1ssu 7608 aptiprleml 7613 mulcomsrg 7731 mulasssrg 7732 distrsrg 7733 aptisr 7753 mulcnsr 7809 cnegex 8109 muladd 8315 lemul12b 8791 qaddcl 9608 iooshf 9923 elfzomelpfzo 10201 expnegzap 10524 setscom 12469 grplmulf1o 12805 cnpnei 13290 cxplt3 13911 cxple3 13912 |
Copyright terms: Public domain | W3C validator |