Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adantrl | GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
adant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
adantrl | ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 103 | . 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓) | |
2 | adant2.1 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | 1, 2 | sylan2 270 | 1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: ad2ant2l 477 ad2ant2rl 480 3ad2antr2 1070 3ad2antr3 1071 xordidc 1290 foco 5116 fvun1 5239 isocnv 5451 isores2 5453 f1oiso2 5466 offval 5719 xp2nd 5793 1stconst 5842 2ndconst 5843 tfrlem9 5935 nnmordi 6089 dom2lem 6252 fundmen 6286 ltsonq 6496 ltexnqq 6506 genprndl 6619 genprndu 6620 ltpopr 6693 ltsopr 6694 ltexprlemm 6698 ltexprlemopl 6699 ltexprlemopu 6701 ltexprlemdisj 6704 ltexprlemfl 6707 ltexprlemfu 6709 mulcmpblnrlemg 6825 cnegexlem2 7187 muladd 7381 divadddivap 7703 ltmul12a 7826 lemul12b 7827 cju 7913 zextlt 8332 xrre 8733 ixxdisj 8772 iooshf 8821 icodisj 8860 iccshftr 8862 iccshftl 8864 iccdil 8866 icccntr 8868 iccf1o 8872 fzaddel 8922 fzsubel 8923 iseqcaopr 9242 expineg2 9264 expsubap 9302 expnbnd 9372 |
Copyright terms: Public domain | W3C validator |