![]() |
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 479 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
3 | 2 | adantll 476 | 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: mpteqb 5619 fiunsnnn 6895 addcomnqg 7394 addassnqg 7395 nqtri3or 7409 lt2addnq 7417 lt2mulnq 7418 enq0ref 7446 enq0tr 7447 nqnq0pi 7451 nqpnq0nq 7466 nqnq0a 7467 distrnq0 7472 addassnq0lemcl 7474 ltsrprg 7760 mulcomsrg 7770 mulasssrg 7771 distrsrg 7772 aptisr 7792 mulcnsr 7848 cnegex 8149 sub4 8216 muladd 8355 ltleadd 8417 divdivdivap 8684 divadddivap 8698 ltmul12a 8831 fzrev 10098 facndiv 10733 cncongr1 12117 ghmeql 13161 blbas 14286 cncfmet 14432 ptolemy 14598 |
Copyright terms: Public domain | W3C validator |