![]() |
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 108 | . 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓) | |
2 | adant2.1 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | 1, 2 | sylan2 280 | 1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: ad2ant2l 492 ad2ant2rl 495 3ad2antr2 1105 3ad2antr3 1106 xordidc 1331 foco 5141 fvun1 5265 isocnv 5476 isores2 5478 f1oiso2 5491 offval 5744 xp2nd 5818 1stconst 5867 2ndconst 5868 tfrlem9 5962 nnmordi 6148 dom2lem 6311 fundmen 6345 ltsonq 6639 ltexnqq 6649 genprndl 6762 genprndu 6763 ltpopr 6836 ltsopr 6837 ltexprlemm 6841 ltexprlemopl 6842 ltexprlemopu 6844 ltexprlemdisj 6847 ltexprlemfl 6850 ltexprlemfu 6852 mulcmpblnrlemg 6968 cnegexlem2 7340 muladd 7544 divadddivap 7871 ltmul12a 7994 lemul12b 7995 cju 8094 zextlt 8509 supinfneg 8753 infsupneg 8754 xrre 8952 ixxdisj 8991 iooshf 9040 icodisj 9079 iccshftr 9081 iccshftl 9083 iccdil 9085 icccntr 9087 iccf1o 9091 fzaddel 9142 fzsubel 9143 iseqcaopr 9547 expineg2 9571 expsubap 9610 expnbnd 9682 facndiv 9752 lcmdvds 10594 |
Copyright terms: Public domain | W3C validator |