HomeHome Intuitionistic Logic Explorer
Theorem List (p. 4 of 22)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 301-400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorempm5.42 301 Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 
Theoremancr 302 Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
 
Theoremancrb 303 Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
 
Theoremancli 304 Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
   =>   
 
Theoremancri 305 Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
   =>   
 
Theoremancld 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.)
   =>   
 
Theoremancrd 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.)
   =>   
 
Theoremanc2l 308 Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.)
 
Theoremanc2r 309 Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
 
Theoremanc2li 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.)
   =>   
 
Theoremanc2ri 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.)
   =>   
 
Theorempm3.41 312 Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
 
Theorempm3.42 313 Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
 
Theorempm3.4 314 Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
 
Theorempm4.45im 315 Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
 
Theoremanim12d 316 Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
   &       =>   
 
Theoremanim1d 317 Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
   =>   
 
Theoremanim2d 318 Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremanim12i 319 Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
   &       =>   
 
Theoremanim1i 320 Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremanim2i 321 Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremanim12ii 322 Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.)
   &       =>   
 
Theoremprth 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.)
 
Theorempm3.33 324 Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
 
Theorempm3.34 325 Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
 
Theorempm3.35 326 Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
 
Theorempm5.31 327 Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 
Theoremimp4a 328 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp4b 329 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp4c 330 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp4d 331 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp41 332 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp42 333 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp43 334 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp44 335 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp45 336 An importation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremimp5a 337 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremimp5d 338 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremimp5g 339 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremimp55 340 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremimp511 341 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremexpimpd 342 Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
   =>   
 
Theoremexp31 343 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp32 344 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp4a 345 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp4b 346 An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
   =>   
 
Theoremexp4c 347 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp4d 348 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp41 349 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp42 350 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp43 351 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp44 352 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexp45 353 An exportation inference. (Contributed by NM, 26-Apr-1994.)
   =>   
 
Theoremexpr 354 Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
   =>   
 
Theoremexp5c 355 An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremexp53 356 An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
   =>   
 
Theoremexpl 357 Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
   =>   
 
Theoremimpr 358 Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
   =>   
 
Theoremimpl 359 Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
   =>   
 
Theoremimpac 360 Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)
   =>   
 
Theoremexbiri 361 Inference form of exbir 1253. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
   =>   
 
Theoremsimprbda 362 Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
   =>   
 
Theoremsimplbda 363 Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
   =>   
 
Theoremsimplbi2 364 Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
   =>   
 
Theoremdfbi2 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.)
 
Theorempm4.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.)
 
Theorempm4.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.)
 
Theorempm4.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.)
   =>   
 
Theorempm4.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.)
   =>   
 
Theorempm4.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.)
   =>   
 
Theorempm4.24 371 Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 14-Mar-2014.)
 
Theoremanidm 372 Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
 
TheoremanidmOLD 373 Obsolete proof of anidm 372 as of 14-Mar-2014. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 6-Nov-2012.)
 
Theorempm4.24OLD 374 Obsolete proof of pm4.24 371 as of 14-Mar-2014. (Contributed by NM, 3-Jan-2005.)
 
Theoremanidms 375 Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
   =>   
 
Theoremanidmdbi 376 Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
 
Theoremanasss 377 Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
   =>   
 
Theoremanassrs 378 Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
   =>   
 
Theoremanass 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.)
 
Theoremsylanl1 380 A syllogism inference. (Contributed by NM, 10-Mar-2005.)
   &       =>   
 
Theoremsylanl2 381 A syllogism inference. (Contributed by NM, 1-Jan-2005.)
   &       =>   
 
Theoremsylanr1 382 A syllogism inference. (Contributed by NM, 9-Apr-2005.)
   &       =>   
 
Theoremsylanr2 383 A syllogism inference. (Contributed by NM, 9-Apr-2005.)
   &       =>   
 
Theoremsylani 384 A syllogism inference. (Contributed by NM, 2-May-1996.)
   &       =>   
 
Theoremsylan2i 385 A syllogism inference. (Contributed by NM, 1-Aug-1994.)
   &       =>   
 
Theoremsyl2ani 386 A syllogism inference. (Contributed by NM, 3-Aug-1999.)
   &       &       =>   
 
Theoremsylan9 387 Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
   &       =>   
 
Theoremsylan9r 388 Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.)
   &       =>   
 
Theoremsyl2anc 389 Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
   &       &       =>   
 
Theoremsylancl 390 Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
   &       &       =>   
 
Theoremsylancr 391 Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
   &       &       =>   
 
Theoremsylanbrc 392 Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
   &       &       =>   
 
Theoremsylancb 393 A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
   &       &       =>   
 
Theoremsylancbr 394 A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.)
   &       &       =>   
 
Theoremsylancom 395 Syllogism inference with commutation of antecents. (Contributed by NM, 2-Jul-2008.)
   &       =>   
 
Theoremmpdan 396 An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
   &       =>   
 
Theoremmpancom 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.)
   &       =>   
 
Theoremmpan 398 An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
   &       =>   
 
Theoremmpan2 399 An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
   &       =>   
 
Theoremmp2an 400 An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
   &       &       =>   
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2186
  Copyright terms: Public domain < Previous  Next >