![]() |
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 463 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantlr 462 | 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: fvtp1g 5544 fcof1o 5606 infnfi 6691 addcomnqg 7037 addassnqg 7038 nqtri3or 7052 ltexnqq 7064 nqnq0pi 7094 nqpnq0nq 7109 nqnq0a 7110 addassnq0lemcl 7117 ltaddpr 7253 ltexprlemloc 7263 addcanprlemu 7271 recexprlem1ssu 7290 aptiprleml 7295 mulcomsrg 7400 mulasssrg 7401 distrsrg 7402 aptisr 7421 mulcnsr 7469 cnegex 7757 muladd 7959 lemul12b 8419 qaddcl 9219 iooshf 9518 elfzomelpfzo 9791 expnegzap 10104 setscom 11683 cnpnei 12070 |
Copyright terms: Public domain | W3C validator |