![]() |
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 109 | . 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓) | |
2 | adant2.1 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | 1, 2 | sylan2 282 | 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: ad2ant2l 497 ad2ant2rl 500 3ad2antr2 1128 3ad2antr3 1129 xordidc 1358 foco 5311 fvun1 5439 isocnv 5664 isores2 5666 f1oiso2 5680 offval 5941 xp2nd 6016 1stconst 6070 2ndconst 6071 tfrlem9 6168 nnmordi 6364 dom2lem 6618 fundmen 6652 mapen 6691 ssenen 6696 ltsonq 7148 ltexnqq 7158 genprndl 7271 genprndu 7272 ltpopr 7345 ltsopr 7346 ltexprlemm 7350 ltexprlemopl 7351 ltexprlemopu 7353 ltexprlemdisj 7356 ltexprlemfl 7359 ltexprlemfu 7361 mulcmpblnrlemg 7477 cnegexlem2 7855 muladd 8059 eqord1 8158 eqord2 8159 divadddivap 8394 ltmul12a 8522 lemul12b 8523 cju 8623 zextlt 9041 supinfneg 9286 infsupneg 9287 xrre 9490 ixxdisj 9573 iooshf 9622 icodisj 9662 iccshftr 9664 iccshftl 9666 iccdil 9668 icccntr 9670 iccf1o 9674 fzaddel 9726 fzsubel 9727 seq3caopr 10143 expineg2 10189 expsubap 10228 expnbnd 10302 facndiv 10372 hashfacen 10466 lcmdvds 11600 hashdvds 11736 txlm 12284 blininf 12407 xmeter 12419 xmetresbl 12423 limcimo 12584 |
Copyright terms: Public domain | W3C validator |