Type | Label | Description |
Statement |
|
Theorem | 3imtr4i 201 |
A mixed syllogism inference, useful for applying a definition to both
sides of an implication. (Contributed by NM, 5-Aug-1993.)
|
         |
|
Theorem | 3imtr3d 202 |
More general version of 3imtr3i 200. Useful for converting conditional
definitions in a formula. (Contributed by NM, 8-Apr-1996.)
|
             
   |
|
Theorem | 3imtr4d 203 |
More general version of 3imtr4i 201. Useful for converting conditional
definitions in a formula. (Contributed by NM, 26-Oct-1995.)
|
             
   |
|
Theorem | 3imtr3g 204 |
More general version of 3imtr3i 200. Useful for converting definitions
in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by
Wolf Lammen, 20-Dec-2013.)
|
             |
|
Theorem | 3imtr4g 205 |
More general version of 3imtr4i 201. Useful for converting definitions
in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by
Wolf Lammen, 20-Dec-2013.)
|
             |
|
Theorem | 3bitri 206 |
A chained inference from transitive law for logical equivalence.
(Contributed by NM, 5-Aug-1993.)
|
         |
|
Theorem | 3bitrri 207 |
A chained inference from transitive law for logical equivalence.
(Contributed by NM, 4-Aug-2006.)
|
         |
|
Theorem | 3bitr2i 208 |
A chained inference from transitive law for logical equivalence.
(Contributed by NM, 4-Aug-2006.)
|
         |
|
Theorem | 3bitr2ri 209 |
A chained inference from transitive law for logical equivalence.
(Contributed by NM, 4-Aug-2006.)
|
         |
|
Theorem | 3bitr3i 210 |
A chained inference from transitive law for logical equivalence.
(Contributed by NM, 19-Aug-1993.)
|
         |
|
Theorem | 3bitr3ri 211 |
A chained inference from transitive law for logical equivalence.
(Contributed by NM, 5-Aug-1993.)
|
         |
|
Theorem | 3bitr4i 212 |
A chained inference from transitive law for logical equivalence. This
inference is frequently used to apply a definition to both sides of a
logical equivalence. (Contributed by NM, 5-Aug-1993.)
|
         |
|
Theorem | 3bitr4ri 213 |
A chained inference from transitive law for logical equivalence.
(Contributed by NM, 2-Sep-1995.)
|
         |
|
Theorem | 3bitrd 214 |
Deduction from transitivity of biconditional. (Contributed by NM,
13-Aug-1999.)
|
                 |
|
Theorem | 3bitrrd 215 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
                 |
|
Theorem | 3bitr2d 216 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
                 |
|
Theorem | 3bitr2rd 217 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
                 |
|
Theorem | 3bitr3d 218 |
Deduction from transitivity of biconditional. Useful for converting
conditional definitions in a formula. (Contributed by NM,
24-Apr-1996.)
|
                 |
|
Theorem | 3bitr3rd 219 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
                 |
|
Theorem | 3bitr4d 220 |
Deduction from transitivity of biconditional. Useful for converting
conditional definitions in a formula. (Contributed by NM,
18-Oct-1995.)
|
                 |
|
Theorem | 3bitr4rd 221 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
                 |
|
Theorem | 3bitr3g 222 |
More general version of 3bitr3i 210. Useful for converting definitions
in a formula. (Contributed by NM, 4-Jun-1995.)
|
             |
|
Theorem | 3bitr4g 223 |
More general version of 3bitr4i 212. Useful for converting definitions
in a formula. (Contributed by NM, 5-Aug-1993.)
|
             |
|
Theorem | bi3ant 224 |
Construct a biconditional in antecedent position. (Contributed by Wolf
Lammen, 14-May-2013.)
|
      
     
        |
|
Theorem | bisym 225 |
Express symmetries of theorems in terms of biconditionals. (Contributed
by Wolf Lammen, 14-May-2013.)
|
                       |
|
Theorem | imbi2i 226 |
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 227 |
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 228 |
Inference adding a biconditional to the right in an equivalence.
(Contributed by NM, 5-Aug-1993.)
|
         |
|
Theorem | bibi12i 229 |
The equivalence of two equivalences. (Contributed by NM,
5-Aug-1993.)
|
           |
|
Theorem | imbi2d 230 |
Deduction adding an antecedent to both sides of a logical equivalence.
(Contributed by NM, 5-Aug-1993.)
|
        
    |
|
Theorem | imbi1d 231 |
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 232 |
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 233 |
Deduction adding a biconditional to the right in an equivalence.
(Contributed by NM, 5-Aug-1993.)
|
             |
|
Theorem | imbi12d 234 |
Deduction joining two equivalences to form equivalence of implications.
(Contributed by NM, 5-Aug-1993.)
|
            
    |
|
Theorem | bibi12d 235 |
Deduction joining two equivalences to form equivalence of
biconditionals. (Contributed by NM, 5-Aug-1993.)
|
                 |
|
Theorem | imbi1 236 |
Theorem *4.84 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.)
|
    
 
    |
|
Theorem | imbi2 237 |
Theorem *4.85 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
|
      
    |
|
Theorem | imbi1i 238 |
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 239 |
Join two logical equivalences to form equivalence of implications.
(Contributed by NM, 5-Aug-1993.)
|
           |
|
Theorem | bibi1 240 |
Theorem *4.86 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.)
|
    
      |
|
Theorem | biimt 241 |
A wff is equivalent to itself with true antecedent. (Contributed by NM,
28-Jan-1996.)
|
       |
|
Theorem | pm5.5 242 |
Theorem *5.5 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
  
    |
|
Theorem | a1bi 243 |
Inference introducing a theorem as an antecedent. (Contributed by NM,
5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
|
     |
|
Theorem | pm5.501 244 |
Theorem *5.501 of [WhiteheadRussell]
p. 125. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 24-Jan-2013.)
|
       |
|
Theorem | ibib 245 |
Implication in terms of implication and biconditional. (Contributed by
NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
|
         |
|
Theorem | ibibr 246 |
Implication in terms of implication and biconditional. (Contributed by
NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.)
|
         |
|
Theorem | tbt 247 |
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 248 |
Logical equivalence of commuted antecedents. Part of Theorem *4.87 of
[WhiteheadRussell] p. 122.
(Contributed by NM, 5-Aug-1993.)
|
  
        |
|
Theorem | pm5.4 249 |
Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell]
p. 125. (Contributed by NM, 5-Aug-1993.)
|
         |
|
Theorem | imdi 250 |
Distributive law for implication. Compare Theorem *5.41 of
[WhiteheadRussell] p. 125.
(Contributed by NM, 5-Aug-1993.)
|
  
    
     |
|
Theorem | pm5.41 251 |
Theorem *5.41 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.)
|
        
    |
|
Theorem | imbibi 252 |
The antecedent of one side of a biconditional can be moved out of the
biconditional to become the antecedent of the remaining biconditional.
(Contributed by BJ, 1-Jan-2025.) (Proof shortened by Wolf Lammen,
5-Jan-2025.)
|
           |
|
Theorem | imim21b 253 |
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 | impd 254 |
Importation deduction. (Contributed by NM, 31-Mar-1994.)
|
             |
|
Theorem | impcomd 255 |
Importation deduction with commuted antecedents. (Contributed by Peter
Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.)
|
             |
|
Theorem | imp31 256 |
An importation inference. (Contributed by NM, 26-Apr-1994.)
|
        
    |
|
Theorem | imp32 257 |
An importation inference. (Contributed by NM, 26-Apr-1994.)
|
          
  |
|
Theorem | expd 258 |
Exportation deduction. (Contributed by NM, 20-Aug-1993.)
|
       
     |
|
Theorem | expdimp 259 |
A deduction version of exportation, followed by importation.
(Contributed by NM, 6-Sep-2008.)
|
             |
|
Theorem | impancom 260 |
Mixed importation/commutation inference. (Contributed by NM,
22-Jun-2013.)
|
             |
|
Theorem | pm3.3 261 |
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 262 |
Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed
by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|
  
 
      |
|
Theorem | impexp 263 |
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 264 |
Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell]
p. 111. (Contributed by NM, 5-Aug-1993.)
|
       |
|
Theorem | pm3.22 265 |
Theorem *3.22 of [WhiteheadRussell] p.
111. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
|
       |
|
Theorem | ancom 266 |
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 267 |
Commutation of conjuncts in consequent. (Contributed by Jeff Hankins,
14-Aug-2009.)
|
    
    |
|
Theorem | ancoms 268 |
Inference commuting conjunction in antecedent. (Contributed by NM,
21-Apr-1994.)
|
      
  |
|
Theorem | ancomsd 269 |
Deduction commuting conjunction in antecedent. (Contributed by NM,
12-Dec-2004.)
|
             |
|
Theorem | biancomi 270 |
Commuting conjunction in a biconditional. (Contributed by Peter Mazsa,
17-Jun-2018.)
|
         |
|
Theorem | biancomd 271 |
Commuting conjunction in a biconditional, deduction form. (Contributed
by Peter Mazsa, 3-Oct-2018.)
|
             |
|
Theorem | pm3.2i 272 |
Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
|
   |
|
Theorem | pm3.43i 273 |
Nested conjunction of antecedents. (Contributed by NM, 5-Aug-1993.)
|
  
          |
|
Theorem | simplbi 274 |
Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
|
       |
|
Theorem | simprbi 275 |
Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
|
       |
|
Theorem | adantr 276 |
Inference adding a conjunct to the right of an antecedent. (Contributed
by NM, 30-Aug-1993.)
|
   
   |
|
Theorem | adantl 277 |
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 278 |
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 279 |
Deduction adding a conjunct to the right of an antecedent. (Contributed
by NM, 4-May-1994.)
|
           |
|
Theorem | impel 280 |
An inference for implication elimination. (Contributed by Giovanni
Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen,
2-Sep-2020.)
|
           |
|
Theorem | mpan9 281 |
Modus ponens conjoining dissimilar antecedents. (Contributed by NM,
1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|
           |
|
Theorem | syldan 282 |
A syllogism deduction with conjoined antecents. (Contributed by NM,
24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
|
         
   |
|
Theorem | sylan 283 |
A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof
shortened by Wolf Lammen, 22-Nov-2012.)
|
           |
|
Theorem | sylanb 284 |
A syllogism inference. (Contributed by NM, 18-May-1994.)
|
       
   |
|
Theorem | sylanbr 285 |
A syllogism inference. (Contributed by NM, 18-May-1994.)
|
       
   |
|
Theorem | sylan2 286 |
A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof
shortened by Wolf Lammen, 22-Nov-2012.)
|
        
  |
|
Theorem | sylan2b 287 |
A syllogism inference. (Contributed by NM, 21-Apr-1994.)
|
           |
|
Theorem | sylan2br 288 |
A syllogism inference. (Contributed by NM, 21-Apr-1994.)
|
           |
|
Theorem | syl2an 289 |
A double syllogism inference. (Contributed by NM, 31-Jan-1997.)
|
         
   |
|
Theorem | syl2anr 290 |
A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
|
             |
|
Theorem | syl2anb 291 |
A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
|
         
   |
|
Theorem | syl2anbr 292 |
A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
|
         
   |
|
Theorem | syland 293 |
A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|
                 |
|
Theorem | sylan2d 294 |
A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|
            
    |
|
Theorem | syl2and 295 |
A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|
              
      |
|
Theorem | biimpa 296 |
Inference from a logical equivalence. (Contributed by NM,
3-May-1994.)
|
         |
|
Theorem | biimpar 297 |
Inference from a logical equivalence. (Contributed by NM,
3-May-1994.)
|
         |
|
Theorem | biimpac 298 |
Inference from a logical equivalence. (Contributed by NM,
3-May-1994.)
|
         |
|
Theorem | biimparc 299 |
Inference from a logical equivalence. (Contributed by NM,
3-May-1994.)
|
         |
|
Theorem | iba 300 |
Introduction of antecedent as conjunct. Theorem *4.73 of
[WhiteheadRussell] p. 121.
(Contributed by NM, 30-Mar-1994.) (Revised by
NM, 24-Mar-2013.)
|
       |