![]() |
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 5745 fcof1o 5811 infnfi 6924 addcomnqg 7411 addassnqg 7412 nqtri3or 7426 ltexnqq 7438 nqnq0pi 7468 nqpnq0nq 7483 nqnq0a 7484 addassnq0lemcl 7491 ltaddpr 7627 ltexprlemloc 7637 addcanprlemu 7645 recexprlem1ssu 7664 aptiprleml 7669 mulcomsrg 7787 mulasssrg 7788 distrsrg 7789 aptisr 7809 mulcnsr 7865 cnegex 8166 muladd 8372 lemul12b 8849 qaddcl 9667 iooshf 9984 elfzomelpfzo 10263 expnegzap 10588 setscom 12555 grplmulf1o 13033 lmodfopne 13659 cnpnei 14196 cxplt3 14817 cxple3 14818 |
Copyright terms: Public domain | W3C validator |