![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adantrl | Unicode 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: ![]() ![]() |
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 1165 3ad2antr3 1166 xordidc 1410 foco 5467 fvun1 5603 isocnv 5833 isores2 5835 f1oiso2 5849 offval 6114 xp2nd 6191 1stconst 6246 2ndconst 6247 tfrlem9 6344 nnmordi 6541 dom2lem 6798 fundmen 6832 mapen 6874 ssenen 6879 ltsonq 7427 ltexnqq 7437 genprndl 7550 genprndu 7551 ltpopr 7624 ltsopr 7625 ltexprlemm 7629 ltexprlemopl 7630 ltexprlemopu 7632 ltexprlemdisj 7635 ltexprlemfl 7638 ltexprlemfu 7640 mulcmpblnrlemg 7769 cnegexlem2 8163 muladd 8371 eqord1 8470 eqord2 8471 divadddivap 8714 ltmul12a 8847 lemul12b 8848 cju 8948 zextlt 9375 supinfneg 9625 infsupneg 9626 xrre 9850 ixxdisj 9933 iooshf 9982 icodisj 10022 iccshftr 10024 iccshftl 10026 iccdil 10028 icccntr 10030 iccf1o 10034 fzaddel 10089 fzsubel 10090 seq3caopr 10514 expineg2 10560 expsubap 10599 expnbnd 10675 facndiv 10751 hashfacen 10848 fprodeq0 11657 lcmdvds 12111 hashdvds 12253 eulerthlemh 12263 pceu 12327 pcqcl 12338 infpnlem1 12391 4sqlem11 12433 mhmpropd 12918 subsubm 12935 grplcan 13006 grplmulf1o 13018 dfgrp3mlem 13042 mulgfng 13066 mulgsubcl 13076 subsubg 13136 eqger 13163 resghm 13199 conjghm 13215 subsubrng 13561 subsubrg 13592 txlm 14236 blininf 14381 xmeter 14393 xmetresbl 14397 limcimo 14591 |
Copyright terms: Public domain | W3C validator |