HomeTheorem List (p. 4 of 108)
Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 4 of 108) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | jcad 301 | Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
          ![/\](wedge.gif "/\"){kind=small} | ||
| Theorem | jca31 302 | Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.) |
| | ||
| Theorem | jca32 303 | Join three consequents. (Contributed by FL, 1-Aug-2009.) |
| | ||
| Theorem | jcai 304 | Deduction replacing implication with conjunction. (Contributed by NM, 5-Aug-1993.) |
| | ||
| Theorem | jctil 305 | Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
| | ||
| Theorem | jctir 306 | Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
| | ||
| Theorem | jctl 307 | Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) |
| | ||
| Theorem | jctr 308 | Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) |
| | ||
| Theorem | jctild 309 | Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
| | ||
| Theorem | jctird 310 | Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
| | ||
| Theorem | ancl 311 | Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.) |
|
| ||
| Theorem | anclb 312 | Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
| ||
| Theorem | pm5.42 313 | Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
|
| ||
| Theorem | ancr 314 | Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
|
| ||
| Theorem | ancrb 315 | Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
| | ||
| Theorem | ancli 316 | Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.) |
| | ||
| Theorem | ancri 317 | Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
| | ||
| Theorem | ancld 318 | Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
|
| ||
| Theorem | ancrd 319 | Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
|
| ||
| Theorem | anc2l 320 | Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.) |
|
| ||
| Theorem | anc2r 321 | Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) |
|
| ||
| Theorem | anc2li 322 | Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.) |
|
| ||
| Theorem | anc2ri 323 | Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.) |
|
| ||
| Theorem | pm3.41 324 | Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
|
| ||
| Theorem | pm3.42 325 | Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
|
| ||
| Theorem | pm3.4 326 | Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.) |
| | ||
| Theorem | pm4.45im 327 | Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.) |
| | ||
| Theorem | anim12d 328 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |
 | ||
| Theorem | anim1d 329 | Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |
| | ||
| Theorem | anim2d 330 | Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.) |
| | ||
| Theorem | anim12i 331 | Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.) |
| | ||
| Theorem | anim12ci 332 | Variant of anim12i 331 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| | ||
| Theorem | anim1i 333 | Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
|
| ||
| Theorem | anim2i 334 | Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
| | ||
| Theorem | anim12ii 335 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.) |
| | ||
| Theorem | prth 336 | Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema' (splendid theorem). (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
| | ||
| Theorem | pm3.33 337 | Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |
|
| ||
| Theorem | pm3.34 338 | Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |
|
| ||
| Theorem | pm3.35 339 | Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.) |
| | ||
| Theorem | pm5.31 340 | Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
|
| ||
| Theorem | imp4a 341 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp4b 342 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp4c 343 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp4d 344 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp41 345 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp42 346 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp43 347 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp44 348 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp45 349 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | imp5a 350 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
 | ||
| Theorem | imp5d 351 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | imp5g 352 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | imp55 353 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | imp511 354 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | expimpd 355 | Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.) |
| | ||
| Theorem | exp31 356 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
| | ||
| Theorem | exp32 357 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
| | ||
| Theorem | exp4a 358 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp4b 359 | An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
|
| ||
| Theorem | exp4c 360 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp4d 361 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp41 362 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp42 363 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp43 364 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp44 365 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | exp45 366 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
|
| ||
| Theorem | expr 367 | Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
| | ||
| Theorem | exp5c 368 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
|
| ||
| Theorem | exp53 369 | An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.) |
|
| ||
| Theorem | expl 370 | Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.) |
| | ||
| Theorem | impr 371 | Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
| | ||
| Theorem | impl 372 | Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.) |
|
| ||
| Theorem | impac 373 | Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.) |
| | ||
| Theorem | exbiri 374 | Inference form of exbir 1365. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.) |
|
| ||
| Theorem | simprbda 375 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
| | ||
| Theorem | simplbda 376 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
| | ||
| Theorem | simplbi2 377 | Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.) |
| | ||
| Theorem | simpl2im 378 | Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) |
|
| ||
| Theorem | simplbiim 379 | Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| | ||
| Theorem | dfbi2 380 | A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
| | ||
| Theorem | pm4.71 381 | Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.) |
| | ||
| Theorem | pm4.71r 382 | Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999.) |
| | ||
| Theorem | pm4.71i 383 | Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.) |
| | ||
| Theorem | pm4.71ri 384 | Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.) |
| | ||
| Theorem | pm4.71d 385 | Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.) |
| | ||
| Theorem | pm4.71rd 386 | Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.) |
| | ||
| Theorem | pm4.24 387 | Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 14-Mar-2014.) |
| | ||
| Theorem | anidm 388 | Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.) |
| | ||
| Theorem | anidms 389 | Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.) |
| | ||
| Theorem | anidmdbi 390 | Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.) |
| | ||
| Theorem | anasss 391 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
| | ||
| Theorem | anassrs 392 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
| | ||
| Theorem | anass 393 | Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
| | ||
| Theorem | sylanl1 394 | A syllogism inference. (Contributed by NM, 10-Mar-2005.) |
| | ||
| Theorem | sylanl2 395 | A syllogism inference. (Contributed by NM, 1-Jan-2005.) |
| | ||
| Theorem | sylanr1 396 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
|
| ||
| Theorem | sylanr2 397 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
|
| ||
| Theorem | sylani 398 | A syllogism inference. (Contributed by NM, 2-May-1996.) |
|
| ||
| Theorem | sylan2i 399 | A syllogism inference. (Contributed by NM, 1-Aug-1994.) |
| | ||
| Theorem | syl2ani 400 | A syllogism inference. (Contributed by NM, 3-Aug-1999.) |
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |