HomeHome Intuitionistic Logic Explorer
Theorem List (p. 4 of 20)
< 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
 
Theoremanclb 301 Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120. (The proof was shortened by Wolf Lammen, 24-Mar-2013.)
 
Theorempm5.42 302 Theorem *5.42 of [WhiteheadRussell] p. 125.
 
Theoremancr 303 Conjoin antecedent to right of consequent.
 
Theoremancrb 304 Conjoin antecedent to right of consequent. (The proof was shortened by Wolf Lammen, 24-Mar-2013.)
 
Theoremancli 305 Deduction conjoining antecedent to left of consequent.
   =>   
 
Theoremancri 306 Deduction conjoining antecedent to right of consequent.
   =>   
 
Theoremancld 307 Deduction conjoining antecedent to left of consequent in nested implication. (The proof was shortened by Wolf Lammen, 1-Nov-2012.)
   =>   
 
Theoremancrd 308 Deduction conjoining antecedent to right of consequent in nested implication. (The proof was shortened by Wolf Lammen, 1-Nov-2012.)
   =>   
 
Theoremanc2l 309 Conjoin antecedent to left of consequent in nested implication. (The proof was shortened by Wolf Lammen, 14-Jul-2013.)
 
Theoremanc2r 310 Conjoin antecedent to right of consequent in nested implication.
 
Theoremanc2li 311 Deduction conjoining antecedent to left of consequent in nested implication. (The proof was shortened by Wolf Lammen, 7-Dec-2012.)
   =>   
 
Theoremanc2ri 312 Deduction conjoining antecedent to right of consequent in nested implication. (The proof was shortened by Wolf Lammen, 7-Dec-2012.)
   =>   
 
Theorempm3.41 313 Theorem *3.41 of [WhiteheadRussell] p. 113.
 
Theorempm3.42 314 Theorem *3.42 of [WhiteheadRussell] p. 113.
 
Theorempm3.4 315 Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113.
 
Theorempm4.45im 316 Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119.
 
Theoremanim12d 317 Conjoin antecedents and consequents in a deduction. (The proof was shortened by Wolf Lammen, 18-Dec-2013.)
   &       =>   
 
Theoremanim1d 318 Add a conjunct to right of antecedent and consequent in a deduction.
   =>   
 
Theoremanim2d 319 Add a conjunct to left of antecedent and consequent in a deduction.
   =>   
 
Theoremanim12i 320 Conjoin antecedents and consequents of two premises. (The proof was shortened by Wolf Lammen, 14-Dec-2013.)
   &       =>   
 
Theoremanim1i 321 Introduce conjunct to both sides of an implication.
   =>   
 
Theoremanim2i 322 Introduce conjunct to both sides of an implication.
   =>   
 
Theoremanim12ii 323 Conjoin antecedents and consequents in a deduction. (The proof was shortened by Wolf Lammen, 19-Jul-2013.)
   &       =>   
 
Theoremprth 324 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). (The proof was shortened by Wolf Lammen, 7-Apr-2013.)
 
Theorempm3.33 325 Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112.
 
Theorempm3.34 326 Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112.
 
Theorempm3.35 327 Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112.
 
Theorempm5.31 328 Theorem *5.31 of [WhiteheadRussell] p. 125.
 
Theoremimp4a 329 An importation inference.
   =>   
 
Theoremimp4b 330 An importation inference.
   =>   
 
Theoremimp4c 331 An importation inference.
   =>   
 
Theoremimp4d 332 An importation inference.
   =>   
 
Theoremimp41 333 An importation inference.
   =>   
 
Theoremimp42 334 An importation inference.
   =>   
 
Theoremimp43 335 An importation inference.
   =>   
 
Theoremimp44 336 An importation inference.
   =>   
 
Theoremimp45 337 An importation inference.
   =>   
 
Theoremimp5a 338 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremimp5d 339 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremimp5g 340 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremimp55 341 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremimp511 342 An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremexpimpd 343 Exportation followed by a deduction version of importation.
   =>   
 
Theoremexp31 344 An exportation inference.
   =>   
 
Theoremexp32 345 An exportation inference.
   =>   
 
Theoremexp4a 346 An exportation inference.
   =>   
 
Theoremexp4b 347 An exportation inference. (The proof was shortened by Wolf Lammen, 23-Nov-2012.)
   =>   
 
Theoremexp4c 348 An exportation inference.
   =>   
 
Theoremexp4d 349 An exportation inference.
   =>   
 
Theoremexp41 350 An exportation inference.
   =>   
 
Theoremexp42 351 An exportation inference.
   =>   
 
Theoremexp43 352 An exportation inference.
   =>   
 
Theoremexp44 353 An exportation inference.
   =>   
 
Theoremexp45 354 An exportation inference.
   =>   
 
Theoremexpr 355 Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
   =>   
 
Theoremexp5c 356 An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
   =>   
 
Theoremexp53 357 An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
   =>   
 
Theoremexpl 358 Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
   =>   
 
Theoremimpr 359 Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
   =>   
 
Theoremimpl 360 Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
   =>   
 
Theoremimpac 361 Importation with conjunction in consequent.
   =>   
 
Theoremexbiri 362 Inference form of exbir 1322. (Contributed by Alan Sare, 31-Dec-2011.) (The proof was shortened by Wolf Lammen, 27-Jan-2013.)
   =>   
 
Theoremsimprbda 363 Deduction eliminating a conjunct.
   =>   
 
Theoremsimplbda 364 Deduction eliminating a conjunct.
   =>   
 
Theoremsimplbi2 365 Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
   =>   
 
Theoremdfbi2 366 A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49.
 
Theoremdfbi 367 Definition df-bi 109 rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional.
 
Theorempm4.71 368 Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (The proof was shortened by Wolf Lammen, 2-Dec-2012.)
 
Theorempm4.71r 369 Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed).
 
Theorempm4.71i 370 Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120.
   =>   
 
Theorempm4.71ri 371 Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed).
   =>   
 
Theorempm4.71rd 372 Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120.
   =>   
 
Theorempm4.24 373 Theorem *4.24 of [WhiteheadRussell] p. 117.
 
Theoremanidm 374 Idempotent law for conjunction. (The proof was shortened by Wolf Lammen, 14-Mar-2014.)
 
TheoremanidmOLD 375 Obsolete proof of anidm 374 as of 14-Mar-2014.
 
Theorempm4.24OLD 376 Obsolete proof of pm4.24 373 as of 14-Mar-2014.
 
Theoremanidms 377 Inference from idempotent law for conjunction.
   =>   
 
Theoremanidmdbi 378 Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
 
Theoremanasss 379 Associative law for conjunction applied to antecedent (eliminates syllogism).
   =>   
 
Theoremanassrs 380 Associative law for conjunction applied to antecedent (eliminates syllogism).
   =>   
 
Theoremanass 381 Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (The proof was shortened by Wolf Lammen, 24-Nov-2012.)
 
Theoremsylanl1 382 A syllogism inference.
   &       =>   
 
Theoremsylanl2 383 A syllogism inference.
   &       =>   
 
Theoremsylanr1 384 A syllogism inference.
   &       =>   
 
Theoremsylanr2 385 A syllogism inference.
   &       =>   
 
Theoremsylani 386 A syllogism inference.
   &       =>   
 
Theoremsylan2i 387 A syllogism inference.
   &       =>   
 
Theoremsyl2ani 388 A syllogism inference.
   &       &       =>   
 
Theoremsylan9 389 Nested syllogism inference conjoining dissimilar antecedents. (The proof was shortened by Andrew Salmon, 7-May-2011.)
   &       =>   
 
Theoremsylan9r 390 Nested syllogism inference conjoining dissimilar antecedents.
   &       =>   
 
Theoremsyl2anc 391 Syllogism inference combined with contraction.
   &       &       =>   
 
Theoremsylancl 392 Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
   &       &       =>   
 
Theoremsylancr 393 Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
   &       &       =>   
 
Theoremsylanbrc 394 Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
   &       &       =>   
 
Theoremsylancb 395 A syllogism inference combined with contraction.
   &       &       =>   
 
Theoremsylancbr 396 A syllogism inference combined with contraction.
   &       &       =>   
 
Theoremsylancom 397 Syllogism inference with commutation of antecents.
   &       =>   
 
Theoremmpdan 398 An inference based on modus ponens. (The proof was shortened by Wolf Lammen, 22-Nov-2012.)
   &       =>   
 
Theoremmpancom 399 An inference based on modus ponens with commutation of antecedents. (The proof was shortened by Wolf Lammen, 7-Apr-2013.)
   &       =>   
 
Theoremmpan 400 An inference based on modus ponens. (The proof was shortened by Wolf Lammen, 7-Apr-2013.)
   &       =>   
    < 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-1914
  Copyright terms: Public domain < Previous  Next >