![]() |
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 466 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
3 | 2 | adantll 463 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: mpteqb 5443 fiunsnnn 6704 addcomnqg 7090 addassnqg 7091 nqtri3or 7105 lt2addnq 7113 lt2mulnq 7114 enq0ref 7142 enq0tr 7143 nqnq0pi 7147 nqpnq0nq 7162 nqnq0a 7163 distrnq0 7168 addassnq0lemcl 7170 ltsrprg 7443 mulcomsrg 7453 mulasssrg 7454 distrsrg 7455 aptisr 7474 mulcnsr 7522 cnegex 7811 sub4 7878 muladd 8013 ltleadd 8075 divdivdivap 8334 divadddivap 8348 ltmul12a 8476 fzrev 9705 facndiv 10326 cncongr1 11577 blbas 12361 cncfmet 12492 |
Copyright terms: Public domain | W3C validator |