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 475 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantlr 474 | 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: fvtp1g 5704 fcof1o 5768 infnfi 6873 addcomnqg 7343 addassnqg 7344 nqtri3or 7358 ltexnqq 7370 nqnq0pi 7400 nqpnq0nq 7415 nqnq0a 7416 addassnq0lemcl 7423 ltaddpr 7559 ltexprlemloc 7569 addcanprlemu 7577 recexprlem1ssu 7596 aptiprleml 7601 mulcomsrg 7719 mulasssrg 7720 distrsrg 7721 aptisr 7741 mulcnsr 7797 cnegex 8097 muladd 8303 lemul12b 8777 qaddcl 9594 iooshf 9909 elfzomelpfzo 10187 expnegzap 10510 setscom 12456 cnpnei 13013 cxplt3 13634 cxple3 13635 |
Copyright terms: Public domain | W3C validator |