![]() |
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 110 | . 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓) | |
2 | adant2.1 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | 1, 2 | sylan2 286 | 1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: ad2ant2l 508 ad2ant2rl 511 3ad2antr2 1163 3ad2antr3 1164 xordidc 1399 foco 5448 fvun1 5582 isocnv 5811 isores2 5813 f1oiso2 5827 offval 6089 xp2nd 6166 1stconst 6221 2ndconst 6222 tfrlem9 6319 nnmordi 6516 dom2lem 6771 fundmen 6805 mapen 6845 ssenen 6850 ltsonq 7396 ltexnqq 7406 genprndl 7519 genprndu 7520 ltpopr 7593 ltsopr 7594 ltexprlemm 7598 ltexprlemopl 7599 ltexprlemopu 7601 ltexprlemdisj 7604 ltexprlemfl 7607 ltexprlemfu 7609 mulcmpblnrlemg 7738 cnegexlem2 8132 muladd 8340 eqord1 8439 eqord2 8440 divadddivap 8683 ltmul12a 8816 lemul12b 8817 cju 8917 zextlt 9344 supinfneg 9594 infsupneg 9595 xrre 9819 ixxdisj 9902 iooshf 9951 icodisj 9991 iccshftr 9993 iccshftl 9995 iccdil 9997 icccntr 9999 iccf1o 10003 fzaddel 10058 fzsubel 10059 seq3caopr 10482 expineg2 10528 expsubap 10567 expnbnd 10643 facndiv 10718 hashfacen 10815 fprodeq0 11624 lcmdvds 12078 hashdvds 12220 eulerthlemh 12230 pceu 12294 pcqcl 12305 infpnlem1 12356 mhmpropd 12856 grplcan 12931 grplmulf1o 12943 dfgrp3mlem 12967 mulgfng 12986 mulgsubcl 12996 subsubg 13055 eqger 13081 subsubrg 13364 txlm 13749 blininf 13894 xmeter 13906 xmetresbl 13910 limcimo 14104 |
Copyright terms: Public domain | W3C validator |