HomeHome New Foundations Explorer
Theorem List (p. 13 of 64)
< Previous  Next >
Bad symbols? Use Firefox
(or GIF version for IE).

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

Theorem List for New Foundations Explorer - 1201-1300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsyl213anc 1201 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (((ψ χ) θ (τ η ζ)) → σ)       (φσ)
 
Theoremsyl231anc 1202 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (((ψ χ) (θ τ η) ζ) → σ)       (φσ)
 
Theoremsyl312anc 1203 Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (((ψ χ θ) τ (η ζ)) → σ)       (φσ)
 
Theoremsyl321anc 1204 Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (((ψ χ θ) (τ η) ζ) → σ)       (φσ)
 
Theoremsyl133anc 1205 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   ((ψ (χ θ τ) (η ζ σ)) → ρ)       (φρ)
 
Theoremsyl313anc 1206 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (((ψ χ θ) τ (η ζ σ)) → ρ)       (φρ)
 
Theoremsyl331anc 1207 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (((ψ χ θ) (τ η ζ) σ) → ρ)       (φρ)
 
Theoremsyl223anc 1208 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (((ψ χ) (θ τ) (η ζ σ)) → ρ)       (φρ)
 
Theoremsyl232anc 1209 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (((ψ χ) (θ τ η) (ζ σ)) → ρ)       (φρ)
 
Theoremsyl322anc 1210 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (((ψ χ θ) (τ η) (ζ σ)) → ρ)       (φρ)
 
Theoremsyl233anc 1211 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (φρ)    &   (((ψ χ) (θ τ η) (ζ σ ρ)) → μ)       (φμ)
 
Theoremsyl323anc 1212 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (φρ)    &   (((ψ χ θ) (τ η) (ζ σ ρ)) → μ)       (φμ)
 
Theoremsyl332anc 1213 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (φρ)    &   (((ψ χ θ) (τ η ζ) (σ ρ)) → μ)       (φμ)
 
Theoremsyl333anc 1214 A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
(φψ)    &   (φχ)    &   (φθ)    &   (φτ)    &   (φη)    &   (φζ)    &   (φσ)    &   (φρ)    &   (φμ)    &   (((ψ χ θ) (τ η ζ) (σ ρ μ)) → λ)       (φλ)
 
Theoremsyl3an1 1215 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(φψ)    &   ((ψ χ θ) → τ)       ((φ χ θ) → τ)
 
Theoremsyl3an2 1216 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(φχ)    &   ((ψ χ θ) → τ)       ((ψ φ θ) → τ)
 
Theoremsyl3an3 1217 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(φθ)    &   ((ψ χ θ) → τ)       ((ψ χ φ) → τ)
 
Theoremsyl3an1b 1218 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(φψ)    &   ((ψ χ θ) → τ)       ((φ χ θ) → τ)
 
Theoremsyl3an2b 1219 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(φχ)    &   ((ψ χ θ) → τ)       ((ψ φ θ) → τ)
 
Theoremsyl3an3b 1220 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(φθ)    &   ((ψ χ θ) → τ)       ((ψ χ φ) → τ)
 
Theoremsyl3an1br 1221 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(ψφ)    &   ((ψ χ θ) → τ)       ((φ χ θ) → τ)
 
Theoremsyl3an2br 1222 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(χφ)    &   ((ψ χ θ) → τ)       ((ψ φ θ) → τ)
 
Theoremsyl3an3br 1223 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(θφ)    &   ((ψ χ θ) → τ)       ((ψ χ φ) → τ)
 
Theoremsyl3an 1224 A triple syllogism inference. (Contributed by NM, 13-May-2004.)
(φψ)    &   (χθ)    &   (τη)    &   ((ψ θ η) → ζ)       ((φ χ τ) → ζ)
 
Theoremsyl3anb 1225 A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
(φψ)    &   (χθ)    &   (τη)    &   ((ψ θ η) → ζ)       ((φ χ τ) → ζ)
 
Theoremsyl3anbr 1226 A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
(ψφ)    &   (θχ)    &   (ητ)    &   ((ψ θ η) → ζ)       ((φ χ τ) → ζ)
 
Theoremsyld3an3 1227 A syllogism inference. (Contributed by NM, 20-May-2007.)
((φ ψ χ) → θ)    &   ((φ ψ θ) → τ)       ((φ ψ χ) → τ)
 
Theoremsyld3an1 1228 A syllogism inference. (Contributed by NM, 7-Jul-2008.)
((χ ψ θ) → φ)    &   ((φ ψ θ) → τ)       ((χ ψ θ) → τ)
 
Theoremsyld3an2 1229 A syllogism inference. (Contributed by NM, 20-May-2007.)
((φ χ θ) → ψ)    &   ((φ ψ θ) → τ)       ((φ χ θ) → τ)
 
Theoremsyl3anl1 1230 A syllogism inference. (Contributed by NM, 24-Feb-2005.)
(φψ)    &   (((ψ χ θ) τ) → η)       (((φ χ θ) τ) → η)
 
Theoremsyl3anl2 1231 A syllogism inference. (Contributed by NM, 24-Feb-2005.)
(φχ)    &   (((ψ χ θ) τ) → η)       (((ψ φ θ) τ) → η)
 
Theoremsyl3anl3 1232 A syllogism inference. (Contributed by NM, 24-Feb-2005.)
(φθ)    &   (((ψ χ θ) τ) → η)       (((ψ χ φ) τ) → η)
 
Theoremsyl3anl 1233 A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
(φψ)    &   (χθ)    &   (τη)    &   (((ψ θ η) ζ) → σ)       (((φ χ τ) ζ) → σ)
 
Theoremsyl3anr1 1234 A syllogism inference. (Contributed by NM, 31-Jul-2007.)
(φψ)    &   ((χ (ψ θ τ)) → η)       ((χ (φ θ τ)) → η)
 
Theoremsyl3anr2 1235 A syllogism inference. (Contributed by NM, 1-Aug-2007.)
(φθ)    &   ((χ (ψ θ τ)) → η)       ((χ (ψ φ τ)) → η)
 
Theoremsyl3anr3 1236 A syllogism inference. (Contributed by NM, 23-Aug-2007.)
(φτ)    &   ((χ (ψ θ τ)) → η)       ((χ (ψ θ φ)) → η)
 
Theorem3impdi 1237 Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
(((φ ψ) (φ χ)) → θ)       ((φ ψ χ) → θ)
 
Theorem3impdir 1238 Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.)
(((φ ψ) (χ ψ)) → θ)       ((φ χ ψ) → θ)
 
Theorem3anidm12 1239 Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
((φ φ ψ) → χ)       ((φ ψ) → χ)
 
Theorem3anidm13 1240 Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
((φ ψ φ) → χ)       ((φ ψ) → χ)
 
Theorem3anidm23 1241 Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
((φ ψ ψ) → χ)       ((φ ψ) → χ)
 
Theorem3ori 1242 Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
(φ ψ χ)       ((¬ φ ¬ ψ) → χ)
 
Theorem3jao 1243 Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
(((φψ) (χψ) (θψ)) → ((φ χ θ) → ψ))
 
Theorem3jaob 1244 Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
(((φ χ θ) → ψ) ↔ ((φψ) (χψ) (θψ)))
 
Theorem3jaoi 1245 Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
(φψ)    &   (χψ)    &   (θψ)       ((φ χ θ) → ψ)
 
Theorem3jaod 1246 Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
(φ → (ψχ))    &   (φ → (θχ))    &   (φ → (τχ))       (φ → ((ψ θ τ) → χ))
 
Theorem3jaoian 1247 Disjunction of 3 antecedents (inference). (Contributed by NM, 14-Oct-2005.)
((φ ψ) → χ)    &   ((θ ψ) → χ)    &   ((τ ψ) → χ)       (((φ θ τ) ψ) → χ)
 
Theorem3jaodan 1248 Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
((φ ψ) → χ)    &   ((φ θ) → χ)    &   ((φ τ) → χ)       ((φ (ψ θ τ)) → χ)
 
Theorem3jaao 1249 Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.)
(φ → (ψχ))    &   (θ → (τχ))    &   (η → (ζχ))       ((φ θ η) → ((ψ τ ζ) → χ))
 
Theoremsyl3an9b 1250 Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.)
(φ → (ψχ))    &   (θ → (χτ))    &   (η → (τζ))       ((φ θ η) → (ψζ))
 
Theorem3orbi123d 1251 Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
(φ → (ψχ))    &   (φ → (θτ))    &   (φ → (ηζ))       (φ → ((ψ θ η) ↔ (χ τ ζ)))
 
Theorem3anbi123d 1252 Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
(φ → (ψχ))    &   (φ → (θτ))    &   (φ → (ηζ))       (φ → ((ψ θ η) ↔ (χ τ ζ)))
 
Theorem3anbi12d 1253 Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
(φ → (ψχ))    &   (φ → (θτ))       (φ → ((ψ θ η) ↔ (χ τ η)))
 
Theorem3anbi13d 1254 Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
(φ → (ψχ))    &   (φ → (θτ))       (φ → ((ψ η θ) ↔ (χ η τ)))
 
Theorem3anbi23d 1255 Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
(φ → (ψχ))    &   (φ → (θτ))       (φ → ((η ψ θ) ↔ (η χ τ)))
 
Theorem3anbi1d 1256 Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
(φ → (ψχ))       (φ → ((ψ θ τ) ↔ (χ θ τ)))
 
Theorem3anbi2d 1257 Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
(φ → (ψχ))       (φ → ((θ ψ τ) ↔ (θ χ τ)))
 
Theorem3anbi3d 1258 Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
(φ → (ψχ))       (φ → ((θ τ ψ) ↔ (θ τ χ)))
 
Theorem3anim123d 1259 Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)
(φ → (ψχ))    &   (φ → (θτ))    &   (φ → (ηζ))       (φ → ((ψ θ η) → (χ τ ζ)))
 
Theorem3orim123d 1260 Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.)
(φ → (ψχ))    &   (φ → (θτ))    &   (φ → (ηζ))       (φ → ((ψ θ η) → (χ τ ζ)))
 
Theoreman6 1261 Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)
(((φ ψ χ) (θ τ η)) ↔ ((φ θ) (ψ τ) (χ η)))
 
Theorem3an6 1262 Analog of an4 797 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(((φ ψ) (χ θ) (τ η)) ↔ ((φ χ τ) (ψ θ η)))
 
Theorem3or6 1263 Analog of or4 514 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
(((φ ψ) (χ θ) (τ η)) ↔ ((φ χ τ) (ψ θ η)))
 
Theoremmp3an1 1264 An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
φ    &   ((φ ψ χ) → θ)       ((ψ χ) → θ)
 
Theoremmp3an2 1265 An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
ψ    &   ((φ ψ χ) → θ)       ((φ χ) → θ)
 
Theoremmp3an3 1266 An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
χ    &   ((φ ψ χ) → θ)       ((φ ψ) → θ)
 
Theoremmp3an12 1267 An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
φ    &   ψ    &   ((φ ψ χ) → θ)       (χθ)
 
Theoremmp3an13 1268 An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
φ    &   χ    &   ((φ ψ χ) → θ)       (ψθ)
 
Theoremmp3an23 1269 An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
ψ    &   χ    &   ((φ ψ χ) → θ)       (φθ)
 
Theoremmp3an1i 1270 An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)
ψ    &   (φ → ((ψ χ θ) → τ))       (φ → ((χ θ) → τ))
 
Theoremmp3anl1 1271 An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
φ    &   (((φ ψ χ) θ) → τ)       (((ψ χ) θ) → τ)
 
Theoremmp3anl2 1272 An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
ψ    &   (((φ ψ χ) θ) → τ)       (((φ χ) θ) → τ)
 
Theoremmp3anl3 1273 An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
χ    &   (((φ ψ χ) θ) → τ)       (((φ ψ) θ) → τ)
 
Theoremmp3anr1 1274 An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
ψ    &   ((φ (ψ χ θ)) → τ)       ((φ (χ θ)) → τ)
 
Theoremmp3anr2 1275 An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)
χ    &   ((φ (ψ χ θ)) → τ)       ((φ (ψ θ)) → τ)
 
Theoremmp3anr3 1276 An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)
θ    &   ((φ (ψ χ θ)) → τ)       ((φ (ψ χ)) → τ)
 
Theoremmp3an 1277 An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
φ    &   ψ    &   χ    &   ((φ ψ χ) → θ)       θ
 
Theoremmpd3an3 1278 An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
((φ ψ) → χ)    &   ((φ ψ χ) → θ)       ((φ ψ) → θ)
 
Theoremmpd3an23 1279 An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
(φψ)    &   (φχ)    &   ((φ ψ χ) → θ)       (φθ)
 
Theoremmp3and 1280 A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)
(φψ)    &   (φχ)    &   (φθ)    &   (φ → ((ψ χ θ) → τ))       (φτ)
 
Theorembiimp3a 1281 Infer implication from a logical equivalence. Similar to biimpa 470. (Contributed by NM, 4-Sep-2005.)
((φ ψ) → (χθ))       ((φ ψ χ) → θ)
 
Theorembiimp3ar 1282 Infer implication from a logical equivalence. Similar to biimpar 471. (Contributed by NM, 2-Jan-2009.)
((φ ψ) → (χθ))       ((φ ψ θ) → χ)
 
Theorem3anandis 1283 Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.)
(((φ ψ) (φ χ) (φ θ)) → τ)       ((φ (ψ χ θ)) → τ)
 
Theorem3anandirs 1284 Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.)
(((φ θ) (ψ θ) (χ θ)) → τ)       (((φ ψ χ) θ) → τ)
 
Theoremecase23d 1285 Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.)
(φ → ¬ χ)    &   (φ → ¬ θ)    &   (φ → (ψ χ θ))       (φψ)
 
Theorem3ecase 1286 Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
φθ)    &   ψθ)    &   χθ)    &   ((φ ψ χ) → θ)       θ
 
1.2.9  Logical 'nand' (Sheffer stroke)
 
Syntaxwnan 1287 Extend wff definition to include alternative denial ('nand').
wff (φ ψ)
 
Definitiondf-nan 1288 Define incompatibility, or alternative denial ('not-and' or 'nand'). This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar. In the second edition of Principia Mathematica (1927), Russell and Whitehead used the Sheffer stroke and suggested it as a replacement for the "or" and "not" operations of the first edition. However, in practice, "or" and "not" are more widely used. After we define the constant true (df-tru 1319) and the constant false (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ⊤ ) ↔ ⊥ ) (trunantru 1354), (( ⊤ ⊥ ) ↔ ⊤ ) (trunanfal 1355), (( ⊥ ⊤ ) ↔ ⊤ ) (falnantru 1356), and (( ⊥ ⊥ ) ↔ ⊤ ) (falnanfal 1357). Contrast with (df-an 360), (df-or 359), (wi 4), and (df-xor 1305) . (Contributed by Jeff Hoffman, 19-Nov-2007.)
((φ ψ) ↔ ¬ (φ ψ))
 
Theoremnanan 1289 Write 'and' in terms of 'nand'. (Contributed by Mario Carneiro, 9-May-2015.)
((φ ψ) ↔ ¬ (φ ψ))
 
Theoremnancom 1290 The 'nand' operator commutes. (Contributed by Mario Carneiro, 9-May-2015.)
((φ ψ) ↔ (ψ φ))
 
Theoremnannan 1291 Lemma for handling nested 'nand's. (Contributed by Jeff Hoffman, 19-Nov-2007.)
((φ (χ ψ)) ↔ (φ → (χ ψ)))
 
Theoremnanim 1292 Show equivalence between implication and the Nicod version. To derive nic-dfim 1434, apply nanbi 1294. (Contributed by Jeff Hoffman, 19-Nov-2007.)
((φψ) ↔ (φ (ψ ψ)))
 
Theoremnannot 1293 Show equivalence between negation and the Nicod version. To derive nic-dfneg 1435, apply nanbi 1294. (Contributed by Jeff Hoffman, 19-Nov-2007.)
ψ ↔ (ψ ψ))
 
Theoremnanbi 1294 Show equivalence between the bidirectional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.)
((φψ) ↔ ((φ ψ) ((φ φ) (ψ ψ))))
 
Theoremnanbi1 1295 Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
((φψ) → ((φ χ) ↔ (ψ χ)))
 
Theoremnanbi2 1296 Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
((φψ) → ((χ φ) ↔ (χ ψ)))
 
Theoremnanbi12 1297 Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
(((φψ) (χθ)) → ((φ χ) ↔ (ψ θ)))
 
Theoremnanbi1i 1298 Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
(φψ)       ((φ χ) ↔ (ψ χ))
 
Theoremnanbi2i 1299 Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
(φψ)       ((χ φ) ↔ (χ ψ))
 
Theoremnanbi12i 1300 Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
(φψ)    &   (χθ)       ((φ χ) ↔ (ψ θ))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-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-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6308
  Copyright terms: Public domain < Previous  Next >