Home | Intuitionistic Logic ExplorerTheorem List (p. 3 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 | 3bitrd 201 | Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.) |

Theorem | 3bitrrd 202 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |

Theorem | 3bitr2d 203 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |

Theorem | 3bitr2rd 204 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |

Theorem | 3bitr3d 205 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.) |

Theorem | 3bitr3rd 206 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |

Theorem | 3bitr4d 207 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.) |

Theorem | 3bitr4rd 208 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |

Theorem | 3bitr3g 209 | More general version of 3bitr3i 197. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.) |

Theorem | 3bitr4g 210 | More general version of 3bitr4i 199. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.) |

Theorem | bi3ant 211 | Construct a bi-conditional in antecedent position. (Contributed by Wolf Lammen, 14-May-2013.) |

Theorem | bisym 212 | Express symmetries of theorems in terms of biconditionals. (Contributed by Wolf Lammen, 14-May-2013.) |

Theorem | imbi2i 213 | Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.) |

Theorem | bibi2i 214 | Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.) |

Theorem | bibi1i 215 | Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.) |

Theorem | bibi12i 216 | The equivalence of two equivalences. (Contributed by NM, 5-Aug-1993.) |

Theorem | imbi2d 217 | Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |

Theorem | imbi1d 218 | Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.) |

Theorem | bibi2d 219 | Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.) |

Theorem | bibi1d 220 | Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.) |

Theorem | imbi12d 221 | Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.) |

Theorem | bibi12d 222 | Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.) |

Theorem | imbi1 223 | Theorem *4.84 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |

Theorem | imbi2 224 | Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.) |

Theorem | imbi1i 225 | Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.) |

Theorem | imbi12i 226 | Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.) |

Theorem | bibi1 227 | Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |

Theorem | biimt 228 | A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.) |

Theorem | pm5.5 229 | Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |

Theorem | a1bi 230 | Inference rule introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |

Theorem | pm5.501 231 | Theorem *5.501 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 24-Jan-2013.) |

Theorem | ibib 232 | Implication in terms of implication and biconditional. (Contributed by NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.) |

Theorem | ibibr 233 | Implication in terms of implication and biconditional. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.) |

Theorem | tbt 234 | A wff is equivalent to its equivalence with truth. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |

Theorem | bi2.04 235 | Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) |

Theorem | pm5.4 236 | Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.) |

Theorem | imdi 237 | Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.) |

Theorem | pm5.41 238 | Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.) |

Theorem | imim21b 239 | Simplify an implication between two implications when the antecedent of the first is a consequence of the antecedent of the second. The reverse form is useful in producing the successor step in induction proofs. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Wolf Lammen, 14-Sep-2013.) |

Theorem | imp3a 240 | Importation deduction. (Contributed by NM, 31-Mar-1994.) (Revised by NM, 24-Mar-2013.) |

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

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

Theorem | exp3a 243 | Exportation deduction. (Contributed by NM, 20-Aug-1993.) (Revised by NM, 24-Mar-2013.) |

Theorem | expdimp 244 | A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.) |

Theorem | impancom 245 | Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.) |

Theorem | pm3.3 246 | Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |

Theorem | pm3.31 247 | Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |

Theorem | impexp 248 | Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |

Theorem | pm3.21 249 | Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) |

Theorem | pm3.22 250 | Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |

Theorem | ancom 251 | Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.) |

Theorem | ancomd 252 | Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.) |

Theorem | ancoms 253 | Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.) |

Theorem | ancomsd 254 | Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.) |

Theorem | pm3.2i 255 | Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.) |

Theorem | pm3.43i 256 | Nested conjunction of antecedents. (Contributed by NM, 5-Aug-1993.) |

Theorem | simplbi 257 | Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |

Theorem | simprbi 258 | Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |

Theorem | adantr 259 | Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.) |

Theorem | adantl 260 | Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |

Theorem | adantld 261 | Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.) |

Theorem | adantrd 262 | Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.) |

Theorem | mpan9 263 | Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.) |

Theorem | syldan 264 | A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.) |

Theorem | sylan 265 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |

Theorem | sylanb 266 | A syllogism inference. (Contributed by NM, 18-May-1994.) |

Theorem | sylanbr 267 | A syllogism inference. (Contributed by NM, 18-May-1994.) |

Theorem | sylan2 268 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |

Theorem | sylan2b 269 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) |

Theorem | sylan2br 270 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) |

Theorem | syl2an 271 | A double syllogism inference. (Contributed by NM, 31-Jan-1997.) |

Theorem | syl2anr 272 | A double syllogism inference. (Contributed by NM, 17-Sep-2013.) |

Theorem | syl2anb 273 | A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |

Theorem | syl2anbr 274 | A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |

Theorem | syland 275 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |

Theorem | sylan2d 276 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |

Theorem | syl2and 277 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |

Theorem | biimpa 278 | Inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |

Theorem | biimpar 279 | Inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |

Theorem | biimpac 280 | Inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |

Theorem | biimparc 281 | Inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |

Theorem | iba 282 | Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) (Revised by NM, 24-Mar-2013.) |

Theorem | ibar 283 | Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) (Revised by NM, 24-Mar-2013.) |

Theorem | biantru 284 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.) |

Theorem | biantrur 285 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.) |

Theorem | biantrud 286 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.) |

Theorem | biantrurd 287 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.) |

Theorem | jca 288 | Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |

Theorem | jcad 289 | Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |

Theorem | jca31 290 | Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.) |

Theorem | jca32 291 | Join three consequents. (Contributed by FL, 1-Aug-2009.) |

Theorem | jcai 292 | Deduction replacing implication with conjunction. (Contributed by NM, 5-Aug-1993.) |

Theorem | jctil 293 | Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |

Theorem | jctir 294 | Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |

Theorem | jctl 295 | 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 296 | 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 297 | Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |

Theorem | jctird 298 | Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |

Theorem | ancl 299 | Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.) |

Theorem | anclb 300 | 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.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |