Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ad2ant2lr | GIF version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.) |
Ref | Expression |
---|---|
ad2ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad2ant2lr | ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantrr 470 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
3 | 2 | adantll 467 | 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: mpteqb 5504 fiunsnnn 6768 addcomnqg 7182 addassnqg 7183 nqtri3or 7197 lt2addnq 7205 lt2mulnq 7206 enq0ref 7234 enq0tr 7235 nqnq0pi 7239 nqpnq0nq 7254 nqnq0a 7255 distrnq0 7260 addassnq0lemcl 7262 ltsrprg 7548 mulcomsrg 7558 mulasssrg 7559 distrsrg 7560 aptisr 7580 mulcnsr 7636 cnegex 7933 sub4 8000 muladd 8139 ltleadd 8201 divdivdivap 8466 divadddivap 8480 ltmul12a 8611 fzrev 9857 facndiv 10478 cncongr1 11773 blbas 12591 cncfmet 12737 ptolemy 12894 |
Copyright terms: Public domain | W3C validator |