P. 6 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 501-600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pm4.25 501	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (φ ↔ (φ ∨ φ))
Theorem	orim12i 502	Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
⊢ (φ → ψ)    &   ⊢ (χ → θ)    ⇒   ⊢ ((φ ∨ χ) → (ψ ∨ θ))
Theorem	orim1i 503	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (φ → ψ)    ⇒   ⊢ ((φ ∨ χ) → (ψ ∨ χ))
Theorem	orim2i 504	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (φ → ψ)    ⇒   ⊢ ((χ ∨ φ) → (χ ∨ ψ))
Theorem	orbi2i 505	Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ((χ ∨ φ) ↔ (χ ∨ ψ))
Theorem	orbi1i 506	Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ((φ ∨ χ) ↔ (ψ ∨ χ))
Theorem	orbi12i 507	Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ θ)    ⇒   ⊢ ((φ ∨ χ) ↔ (ψ ∨ θ))
Theorem	pm1.5 508	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∨ (ψ ∨ χ)) → (ψ ∨ (φ ∨ χ)))
Theorem	or12 509	Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ ((φ ∨ (ψ ∨ χ)) ↔ (ψ ∨ (φ ∨ χ)))
Theorem	orass 510	Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((φ ∨ ψ) ∨ χ) ↔ (φ ∨ (ψ ∨ χ)))
Theorem	pm2.31 511	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∨ (ψ ∨ χ)) → ((φ ∨ ψ) ∨ χ))
Theorem	pm2.32 512	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ ∨ ψ) ∨ χ) → (φ ∨ (ψ ∨ χ)))
Theorem	or32 513	A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((φ ∨ ψ) ∨ χ) ↔ ((φ ∨ χ) ∨ ψ))
Theorem	or4 514	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
⊢ (((φ ∨ ψ) ∨ (χ ∨ θ)) ↔ ((φ ∨ χ) ∨ (ψ ∨ θ)))
Theorem	or42 515	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
⊢ (((φ ∨ ψ) ∨ (χ ∨ θ)) ↔ ((φ ∨ χ) ∨ (θ ∨ ψ)))
Theorem	orordi 516	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ ((φ ∨ (ψ ∨ χ)) ↔ ((φ ∨ ψ) ∨ (φ ∨ χ)))
Theorem	orordir 517	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ (((φ ∨ ψ) ∨ χ) ↔ ((φ ∨ χ) ∨ (ψ ∨ χ)))
Theorem	jca 518	Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Equivalent to the natural deduction rule ∧ I (∧ introduction), see natded in set.mm. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    ⇒   ⊢ (φ → (ψ ∧ χ))
Theorem	jcad 519	Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (ψ → θ))    ⇒   ⊢ (φ → (ψ → (χ ∧ θ)))
Theorem	jca31 520	Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    ⇒   ⊢ (φ → ((ψ ∧ χ) ∧ θ))
Theorem	jca32 521	Join three consequents. (Contributed by FL, 1-Aug-2009.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    ⇒   ⊢ (φ → (ψ ∧ (χ ∧ θ)))
Theorem	jcai 522	Deduction replacing implication with conjunction. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ ∧ χ))
Theorem	jctil 523	Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
⊢ (φ → ψ)    &   ⊢ χ    ⇒   ⊢ (φ → (χ ∧ ψ))
Theorem	jctir 524	Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
⊢ (φ → ψ)    &   ⊢ χ    ⇒   ⊢ (φ → (ψ ∧ χ))
Theorem	jctl 525	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 526	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 527	Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → θ)    ⇒   ⊢ (φ → (ψ → (θ ∧ χ)))
Theorem	jctird 528	Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → θ)    ⇒   ⊢ (φ → (ψ → (χ ∧ θ)))
Theorem	ancl 529	Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ ((φ → ψ) → (φ → (φ ∧ ψ)))
Theorem	anclb 530	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.)
⊢ ((φ → ψ) ↔ (φ → (φ ∧ ψ)))
Theorem	pm5.42 531	Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ → (ψ → χ)) ↔ (φ → (ψ → (φ ∧ χ))))
Theorem	ancr 532	Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ ((φ → ψ) → (φ → (ψ ∧ φ)))
Theorem	ancrb 533	Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((φ → ψ) ↔ (φ → (ψ ∧ φ)))
Theorem	ancli 534	Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
⊢ (φ → ψ)    ⇒   ⊢ (φ → (φ ∧ ψ))
Theorem	ancri 535	Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ (φ → ψ)    ⇒   ⊢ (φ → (ψ ∧ φ))
Theorem	ancld 536	Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → (ψ ∧ χ)))
Theorem	ancrd 537	Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → (χ ∧ ψ)))
Theorem	anc2l 538	Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.)
⊢ ((φ → (ψ → χ)) → (φ → (ψ → (φ ∧ χ))))
Theorem	anc2r 539	Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
⊢ ((φ → (ψ → χ)) → (φ → (ψ → (χ ∧ φ))))
Theorem	anc2li 540	Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → (φ ∧ χ)))
Theorem	anc2ri 541	Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → (χ ∧ φ)))
Theorem	pm3.41 542	Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ → χ) → ((φ ∧ ψ) → χ))
Theorem	pm3.42 543	Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((ψ → χ) → ((φ ∧ ψ) → χ))
Theorem	pm3.4 544	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
⊢ ((φ ∧ ψ) → (φ → ψ))
Theorem	pm4.45im 545	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
⊢ (φ ↔ (φ ∧ (ψ → φ)))
Theorem	anim12d 546	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ → τ))    ⇒   ⊢ (φ → ((ψ ∧ θ) → (χ ∧ τ)))
Theorem	anim1d 547	Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((ψ ∧ θ) → (χ ∧ θ)))
Theorem	anim2d 548	Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ((θ ∧ ψ) → (θ ∧ χ)))
Theorem	anim12i 549	Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
⊢ (φ → ψ)    &   ⊢ (χ → θ)    ⇒   ⊢ ((φ ∧ χ) → (ψ ∧ θ))
Theorem	anim12ci 550	Variant of anim12i 549 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ → ψ)    &   ⊢ (χ → θ)    ⇒   ⊢ ((φ ∧ χ) → (θ ∧ ψ))
Theorem	anim1i 551	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    ⇒   ⊢ ((φ ∧ χ) → (ψ ∧ χ))
Theorem	anim2i 552	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    ⇒   ⊢ ((χ ∧ φ) → (χ ∧ ψ))
Theorem	anim12ii 553	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (ψ → τ))    ⇒   ⊢ ((φ ∧ θ) → (ψ → (χ ∧ τ)))
Theorem	prth 554	Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 546. 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). (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ (((φ → ψ) ∧ (χ → θ)) → ((φ ∧ χ) → (ψ ∧ θ)))
Theorem	pm2.3 555	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∨ (ψ ∨ χ)) → (φ ∨ (χ ∨ ψ)))
Theorem	pm2.41 556	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((ψ ∨ (φ ∨ ψ)) → (φ ∨ ψ))
Theorem	pm2.42 557	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ φ ∨ (φ → ψ)) → (φ → ψ))
Theorem	pm2.4 558	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∨ (φ ∨ ψ)) → (φ ∨ ψ))
Theorem	pm2.65da 559	Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((φ ∧ ψ) → ¬ χ)    ⇒   ⊢ (φ → ¬ ψ)
Theorem	pm4.44 560	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (φ ↔ (φ ∨ (φ ∧ ψ)))
Theorem	pm4.14 561	Theorem *4.14 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.)
⊢ (((φ ∧ ψ) → χ) ↔ ((φ ∧ ¬ χ) → ¬ ψ))
Theorem	pm3.37 562	Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.)
⊢ (((φ ∧ ψ) → χ) → ((φ ∧ ¬ χ) → ¬ ψ))
Theorem	nan 563	Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.)
⊢ ((φ → ¬ (ψ ∧ χ)) ↔ ((φ ∧ ψ) → ¬ χ))
Theorem	pm4.15 564	Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
⊢ (((φ ∧ ψ) → ¬ χ) ↔ ((ψ ∧ χ) → ¬ φ))
Theorem	pm4.78 565	Theorem *4.78 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ (((φ → ψ) ∨ (φ → χ)) ↔ (φ → (ψ ∨ χ)))
Theorem	pm4.79 566	Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.)
⊢ (((ψ → φ) ∨ (χ → φ)) ↔ ((ψ ∧ χ) → φ))
Theorem	pm4.87 567	Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)
⊢ (((((φ ∧ ψ) → χ) ↔ (φ → (ψ → χ))) ∧ ((φ → (ψ → χ)) ↔ (ψ → (φ → χ)))) ∧ ((ψ → (φ → χ)) ↔ ((ψ ∧ φ) → χ)))
Theorem	pm3.33 568	Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
⊢ (((φ → ψ) ∧ (ψ → χ)) → (φ → χ))
Theorem	pm3.34 569	Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
⊢ (((ψ → χ) ∧ (φ → ψ)) → (φ → χ))
Theorem	pm3.35 570	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
⊢ ((φ ∧ (φ → ψ)) → ψ)
Theorem	pm5.31 571	Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((χ ∧ (φ → ψ)) → (φ → (ψ ∧ χ)))
Theorem	imp4a 572	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (φ → (ψ → ((χ ∧ θ) → τ)))
Theorem	imp4b 573	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ ((φ ∧ ψ) → ((χ ∧ θ) → τ))
Theorem	imp4c 574	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (φ → (((ψ ∧ χ) ∧ θ) → τ))
Theorem	imp4d 575	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (φ → ((ψ ∧ (χ ∧ θ)) → τ))
Theorem	imp41 576	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ ((((φ ∧ ψ) ∧ χ) ∧ θ) → τ)
Theorem	imp42 577	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (((φ ∧ (ψ ∧ χ)) ∧ θ) → τ)
Theorem	imp43 578	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)
Theorem	imp44 579	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ ((φ ∧ ((ψ ∧ χ) ∧ θ)) → τ)
Theorem	imp45 580	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ ((φ ∧ (ψ ∧ (χ ∧ θ))) → τ)
Theorem	imp5a 581	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (φ → (ψ → (χ → ((θ ∧ τ) → η))))
Theorem	imp5d 582	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (((φ ∧ ψ) ∧ χ) → ((θ ∧ τ) → η))
Theorem	imp5g 583	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ ((φ ∧ ψ) → (((χ ∧ θ) ∧ τ) → η))
Theorem	imp55 584	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (((φ ∧ (ψ ∧ (χ ∧ θ))) ∧ τ) → η)
Theorem	imp511 585	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ ((φ ∧ ((ψ ∧ (χ ∧ θ)) ∧ τ)) → η)
Theorem	expimpd 586	Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
⊢ ((φ ∧ ψ) → (χ → θ))    ⇒   ⊢ (φ → ((ψ ∧ χ) → θ))
Theorem	exp31 587	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (φ → (ψ → (χ → θ)))
Theorem	exp32 588	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ (φ → (ψ → (χ → θ)))
Theorem	exp4a 589	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (ψ → ((χ ∧ θ) → τ)))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp4b 590	An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
⊢ ((φ ∧ ψ) → ((χ ∧ θ) → τ))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp4c 591	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → (((ψ ∧ χ) ∧ θ) → τ))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp4d 592	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (φ → ((ψ ∧ (χ ∧ θ)) → τ))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp41 593	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((((φ ∧ ψ) ∧ χ) ∧ θ) → τ)    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp42 594	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((φ ∧ (ψ ∧ χ)) ∧ θ) → τ)    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp43 595	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp44 596	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((φ ∧ ((ψ ∧ χ) ∧ θ)) → τ)    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp45 597	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((φ ∧ (ψ ∧ (χ ∧ θ))) → τ)    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	expr 598	Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ ψ) → (χ → θ))
Theorem	exp5c 599	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (φ → ((ψ ∧ χ) → ((θ ∧ τ) → η)))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp53 600	An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((((φ ∧ ψ) ∧ (χ ∧ θ)) ∧ τ) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))