Home | Intuitionistic Logic ExplorerTheorem List (p. 4 of 22)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | pm5.42 301 | Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |

Theorem | ancr 302 | Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |

Theorem | ancrb 303 | Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |

Theorem | ancli 304 | Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.) |

Theorem | ancri 305 | Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |

Theorem | ancld 306 | 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 307 | 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 308 | 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 309 | Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) |

Theorem | anc2li 310 | 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 311 | 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 312 | Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm3.42 313 | Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm3.4 314 | Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.) |

Theorem | pm4.45im 315 | Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.) |

Theorem | anim12d 316 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |

Theorem | anim1d 317 | Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |

Theorem | anim2d 318 | Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | anim12i 319 | Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.) |

Theorem | anim1i 320 | Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |

Theorem | anim2i 321 | Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |

Theorem | anim12ii 322 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.) |

Theorem | prth 323 | 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 324 | Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm3.34 325 | Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm3.35 326 | Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.) |

Theorem | pm5.31 327 | Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |

Theorem | imp4a 328 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp4b 329 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp4c 330 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp4d 331 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp41 332 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp42 333 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp43 334 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp44 335 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp45 336 | An importation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | imp5a 337 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |

Theorem | imp5d 338 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |

Theorem | imp5g 339 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |

Theorem | imp55 340 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |

Theorem | imp511 341 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |

Theorem | expimpd 342 | Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.) |

Theorem | exp31 343 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp32 344 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp4a 345 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp4b 346 | An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |

Theorem | exp4c 347 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp4d 348 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp41 349 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp42 350 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp43 351 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp44 352 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | exp45 353 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |

Theorem | expr 354 | Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |

Theorem | exp5c 355 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |

Theorem | exp53 356 | An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.) |

Theorem | expl 357 | Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.) |

Theorem | impr 358 | Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |

Theorem | impl 359 | Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.) |

Theorem | impac 360 | Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.) |

Theorem | exbiri 361 | Inference form of exbir 1253. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.) |

Theorem | simprbda 362 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |

Theorem | simplbda 363 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |

Theorem | simplbi2 364 | Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.) |

Theorem | dfbi2 365 | 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 366 | 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 367 | 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 368 | 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 369 | 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.71rd 370 | 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 371 | Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 14-Mar-2014.) |

Theorem | anidm 372 | Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.) |

Theorem | anidmOLD 373 | Obsolete proof of anidm 372 as of 14-Mar-2014. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 6-Nov-2012.) |

Theorem | pm4.24OLD 374 | Obsolete proof of pm4.24 371 as of 14-Mar-2014. (Contributed by NM, 3-Jan-2005.) |

Theorem | anidms 375 | Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.) |

Theorem | anidmdbi 376 | Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.) |

Theorem | anasss 377 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |

Theorem | anassrs 378 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |

Theorem | anass 379 | 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 380 | A syllogism inference. (Contributed by NM, 10-Mar-2005.) |

Theorem | sylanl2 381 | A syllogism inference. (Contributed by NM, 1-Jan-2005.) |

Theorem | sylanr1 382 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |

Theorem | sylanr2 383 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |

Theorem | sylani 384 | A syllogism inference. (Contributed by NM, 2-May-1996.) |

Theorem | sylan2i 385 | A syllogism inference. (Contributed by NM, 1-Aug-1994.) |

Theorem | syl2ani 386 | A syllogism inference. (Contributed by NM, 3-Aug-1999.) |

Theorem | sylan9 387 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |

Theorem | sylan9r 388 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) |

Theorem | syl2anc 389 | Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.) |

Theorem | sylancl 390 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | sylancr 391 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | sylanbrc 392 | Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | sylancb 393 | A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.) |

Theorem | sylancbr 394 | A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.) |

Theorem | sylancom 395 | Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.) |

Theorem | mpdan 396 | An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |

Theorem | mpancom 397 | An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |

Theorem | mpan 398 | An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |

Theorem | mpan2 399 | An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |

Theorem | mp2an 400 | An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |