Home | Intuitionistic Logic ExplorerTheorem List (p. 3 of 20)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

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

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

Statement | ||

Theorem | 3bitr4ri 201 | A chained inference from transitive law for logical equivalence. |

Theorem | 3bitrd 202 | Deduction from transitivity of biconditional. |

Theorem | 3bitrrd 203 | Deduction from transitivity of biconditional. |

Theorem | 3bitr2d 204 | Deduction from transitivity of biconditional. |

Theorem | 3bitr2rd 205 | Deduction from transitivity of biconditional. |

Theorem | 3bitr3d 206 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. |

Theorem | 3bitr3rd 207 | Deduction from transitivity of biconditional. |

Theorem | 3bitr4d 208 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. |

Theorem | 3bitr4rd 209 | Deduction from transitivity of biconditional. |

Theorem | 3bitr3g 210 | More general version of 3bitr3i 198. Useful for converting definitions in a formula. |

Theorem | 3bitr4g 211 | More general version of 3bitr4i 200. Useful for converting definitions in a formula. |

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

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

Theorem | imbi2i 214 | Introduce an antecedent to both sides of a logical equivalence. (The proof was shortened by Wolf Lammen, 6-Feb-2013.) |

Theorem | bibi2i 215 | Inference adding a biconditional to the left in an equivalence. (The proof was shortened by Andrew Salmon, 7-May-2011.) (The proof was shortened by Wolf Lammen, 16-May-2013.) |

Theorem | bibi1i 216 | Inference adding a biconditional to the right in an equivalence. |

Theorem | bibi12i 217 | The equivalence of two equivalences. |

Theorem | imbi2d 218 | Deduction adding an antecedent to both sides of a logical equivalence. |

Theorem | imbi1d 219 | Deduction adding a consequent to both sides of a logical equivalence. (The proof was shortened by Wolf Lammen, 17-Sep-2013.) |

Theorem | bibi2d 220 | Deduction adding a biconditional to the left in an equivalence. (The proof was shortened by Wolf Lammen, 19-May-2013.) |

Theorem | bibi1d 221 | Deduction adding a biconditional to the right in an equivalence. |

Theorem | imbi12d 222 | Deduction joining two equivalences to form equivalence of implications. |

Theorem | bibi12d 223 | Deduction joining two equivalences to form equivalence of biconditionals. |

Theorem | imbi1 224 | Theorem *4.84 of [WhiteheadRussell] p. 122. |

Theorem | imbi2 225 | Theorem *4.85 of [WhiteheadRussell] p. 122. (The proof was shortened by Wolf Lammen, 19-May-2013.) |

Theorem | imbi1i 226 | Introduce a consequent to both sides of a logical equivalence. (The proof was shortened by Wolf Lammen, 17-Sep-2013.) |

Theorem | imbi12i 227 | Join two logical equivalences to form equivalence of implications. |

Theorem | bibi1 228 | Theorem *4.86 of [WhiteheadRussell] p. 122. |

Theorem | biimt 229 | A wff is equivalent to itself with true antecedent. |

Theorem | pm5.5 230 | Theorem *5.5 of [WhiteheadRussell] p. 125. |

Theorem | a1bi 231 | Inference rule introducing a theorem as an antecedent. The proof was shortened by Wolf Lammen, 11-Nov-2012.) |

Theorem | pm5.501 232 | Theorem *5.501 of [WhiteheadRussell] p. 125. |

Theorem | ibib 233 | Implication in terms of implication and biconditional. (The proof was shortened by Wolf Lammen, 24-Jan-2013.) |

Theorem | ibibr 234 | Implication in terms of implication and biconditional. (The proof was shortened by Wolf Lammen, 21-Dec-2013.) |

Theorem | tbt 235 | A wff is equivalent to its equivalence with truth. (The proof was shortened by Andrew Salmon, 13-May-2011.) |

Theorem | bi2.04 236 | Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. |

Theorem | pm5.4 237 | Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. |

Theorem | imdi 238 | Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. |

Theorem | pm5.41 239 | Theorem *5.41 of [WhiteheadRussell] p. 125. (The proof was shortened by Wolf Lammen, 12-Oct-2012.) |

Theorem | imim21b 240 | 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.) (The proof was shortened by Wolf Lammen, 14-Sep-2013.) |

Theorem | imp3a 241 | Importation deduction. |

Theorem | imp31 242 | An importation inference. |

Theorem | imp32 243 | An importation inference. |

Theorem | exp3a 244 | Exportation deduction. |

Theorem | expdimp 245 | A deduction version of exportation, followed by importation. |

Theorem | impancom 246 | Mixed importation/commutation inference. |

Theorem | pm3.3 247 | Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112. (The proof was shortened by Wolf Lammen, 24-Mar-2013.) |

Theorem | pm3.31 248 | Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (The proof was shortened by Wolf Lammen, 24-Mar-2013.) |

Theorem | impexp 249 | Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (The proof was shortened by Wolf Lammen, 24-Mar-2013.) |

Theorem | pm3.21 250 | Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. |

Theorem | pm3.22 251 | Theorem *3.22 of [WhiteheadRussell] p. 111. (The proof was shortened by Wolf Lammen, 13-Nov-2012.) |

Theorem | ancom 252 | Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (The proof was shortened by Wolf Lammen, 4-Nov-2012.) |

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

Theorem | ancoms 254 | Inference commuting conjunction in antecedent. |

Theorem | ancomsd 255 | Deduction commuting conjunction in antecedent. |

Theorem | pm3.2i 256 | Infer conjunction of premises. |

Theorem | pm3.43i 257 | Nested conjunction of antecedents. |

Theorem | simplbi 258 | Deduction eliminating a conjunct. |

Theorem | simprbi 259 | Deduction eliminating a conjunct. |

Theorem | adantr 260 | Inference adding a conjunct to the right of an antecedent. |

Theorem | adantl 261 | Inference adding a conjunct to the left of an antecedent. (The proof was shortened by Wolf Lammen, 23-Nov-2012.) |

Theorem | adantld 262 | Deduction adding a conjunct to the left of an antecedent. (The proof was shortened by Wolf Lammen, 20-Dec-2012.) |

Theorem | adantrd 263 | Deduction adding a conjunct to the right of an antecedent. |

Theorem | mpan9 264 | Modus ponens conjoining dissimilar antecedents. (The proof was shortened by Andrew Salmon, 7-May-2011.) |

Theorem | syldan 265 | A syllogism deduction with conjoined antecents. (The proof was shortened by Wolf Lammen, 6-Apr-2013.) |

Theorem | sylan 266 | A syllogism inference. (The proof was shortened by Wolf Lammen, 22-Nov-2012.) |

Theorem | sylanb 267 | A syllogism inference. |

Theorem | sylanbr 268 | A syllogism inference. |

Theorem | sylan2 269 | A syllogism inference. (The proof was shortened by Wolf Lammen, 22-Nov-2012.) |

Theorem | sylan2b 270 | A syllogism inference. |

Theorem | sylan2br 271 | A syllogism inference. |

Theorem | syl2an 272 | A double syllogism inference. |

Theorem | syl2anr 273 | A double syllogism inference. |

Theorem | syl2anb 274 | A double syllogism inference. |

Theorem | syl2anbr 275 | A double syllogism inference. |

Theorem | syland 276 | A syllogism deduction. |

Theorem | sylan2d 277 | A syllogism deduction. |

Theorem | syl2and 278 | A syllogism deduction. |

Theorem | biimpa 279 | Inference from a logical equivalence. |

Theorem | biimpar 280 | Inference from a logical equivalence. |

Theorem | biimpac 281 | Inference from a logical equivalence. |

Theorem | biimparc 282 | Inference from a logical equivalence. |

Theorem | iba 283 | Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. |

Theorem | ibar 284 | Introduction of antecedent as conjunct. |

Theorem | biantru 285 | A wff is equivalent to its conjunction with truth. |

Theorem | biantrur 286 | A wff is equivalent to its conjunction with truth. |

Theorem | biantrud 287 | A wff is equivalent to its conjunction with truth. (The proof was shortened by Wolf Lammen, 23-Oct-2013.) |

Theorem | biantrurd 288 | A wff is equivalent to its conjunction with truth. (The proof was shortened by Andrew Salmon, 7-May-2011.) |

Theorem | jca 289 | Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). (The proof was shortened by Wolf Lammen, 25-Oct-2012.) |

Theorem | jcad 290 | Deduction conjoining the consequents of two implications. (The proof was shortened by Wolf Lammen, 23-Jul-2013.) |

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

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

Theorem | jcai 293 | Deduction replacing implication with conjunction. |

Theorem | jctil 294 | Inference conjoining a theorem to left of consequent in an implication. |

Theorem | jctir 295 | Inference conjoining a theorem to right of consequent in an implication. |

Theorem | jctl 296 | Inference conjoining a theorem to the left of a consequent. (The proof was shortened by Wolf Lammen, 24-Oct-2012.) |

Theorem | jctr 297 | Inference conjoining a theorem to the right of a consequent. (The proof was shortened by Wolf Lammen, 24-Oct-2012.) |

Theorem | jctild 298 | Deduction conjoining a theorem to left of consequent in an implication. |

Theorem | jctird 299 | Deduction conjoining a theorem to right of consequent in an implication. |

Theorem | ancl 300 | Conjoin antecedent to left of consequent. |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |