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.)
|- (ph <-> (ph \/ ph))
Theorem	orim12i 502	Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph \/ ch) -> (ps \/ th))
Theorem	orim1i 503	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
|- (ph -> ps)   =>   |- ((ph \/ ch) -> (ps \/ ch))
Theorem	orim2i 504	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
|- (ph -> ps)   =>   |- ((ch \/ ph) -> (ch \/ ps))
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.)
|- (ph <-> ps)   =>   |- ((ch \/ ph) <-> (ch \/ ps))
Theorem	orbi1i 506	Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   =>   |- ((ph \/ ch) <-> (ps \/ ch))
Theorem	orbi12i 507	Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
|- (ph <-> ps)   &   |- (ch <-> th)   =>   |- ((ph \/ ch) <-> (ps \/ th))
Theorem	pm1.5 508	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
|- ((ph \/ (ps \/ ch)) -> (ps \/ (ph \/ ch)))
Theorem	or12 509	Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
|- ((ph \/ (ps \/ ch)) <-> (ps \/ (ph \/ ch)))
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.)
|- (((ph \/ ps) \/ ch) <-> (ph \/ (ps \/ ch)))
Theorem	pm2.31 511	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ((ph \/ (ps \/ ch)) -> ((ph \/ ps) \/ ch))
Theorem	pm2.32 512	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
|- (((ph \/ ps) \/ ch) -> (ph \/ (ps \/ ch)))
Theorem	or32 513	A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (((ph \/ ps) \/ ch) <-> ((ph \/ ch) \/ ps))
Theorem	or4 514	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
|- (((ph \/ ps) \/ (ch \/ th)) <-> ((ph \/ ch) \/ (ps \/ th)))
Theorem	or42 515	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
|- (((ph \/ ps) \/ (ch \/ th)) <-> ((ph \/ ch) \/ (th \/ ps)))
Theorem	orordi 516	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
|- ((ph \/ (ps \/ ch)) <-> ((ph \/ ps) \/ (ph \/ ch)))
Theorem	orordir 517	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
|- (((ph \/ ps) \/ ch) <-> ((ph \/ ch) \/ (ps \/ ch)))
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.)
|- (ph -> ps)   &   |- (ph -> ch)   =>   |- (ph -> (ps /\ ch))
Theorem	jcad 519	Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
|- (ph -> (ps -> ch))   &   |- (ph -> (ps -> th))   =>   |- (ph -> (ps -> (ch /\ th)))
Theorem	jca31 520	Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> th)   =>   |- (ph -> ((ps /\ ch) /\ th))
Theorem	jca32 521	Join three consequents. (Contributed by FL, 1-Aug-2009.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> th)   =>   |- (ph -> (ps /\ (ch /\ th)))
Theorem	jcai 522	Deduction replacing implication with conjunction. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ps)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (ps /\ ch))
Theorem	jctil 523	Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
|- (ph -> ps)   &   |- ch   =>   |- (ph -> (ch /\ ps))
Theorem	jctir 524	Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
|- (ph -> ps)   &   |- ch   =>   |- (ph -> (ps /\ ch))
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.)
|- ps   =>   |- (ph -> (ps /\ ph))
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.)
|- ps   =>   |- (ph -> (ph /\ ps))
Theorem	jctild 527	Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
|- (ph -> (ps -> ch))   &   |- (ph -> th)   =>   |- (ph -> (ps -> (th /\ ch)))
Theorem	jctird 528	Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
|- (ph -> (ps -> ch))   &   |- (ph -> th)   =>   |- (ph -> (ps -> (ch /\ th)))
Theorem	ancl 529	Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.)
|- ((ph -> ps) -> (ph -> (ph /\ ps)))
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.)
|- ((ph -> ps) <-> (ph -> (ph /\ ps)))
Theorem	pm5.42 531	Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> (ps -> ch)) <-> (ph -> (ps -> (ph /\ ch))))
Theorem	ancr 532	Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
|- ((ph -> ps) -> (ph -> (ps /\ ph)))
Theorem	ancrb 533	Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- ((ph -> ps) <-> (ph -> (ps /\ ph)))
Theorem	ancli 534	Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
|- (ph -> ps)   =>   |- (ph -> (ph /\ ps))
Theorem	ancri 535	Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
|- (ph -> ps)   =>   |- (ph -> (ps /\ ph))
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.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ps /\ ch)))
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.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ch /\ ps)))
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.)
|- ((ph -> (ps -> ch)) -> (ph -> (ps -> (ph /\ ch))))
Theorem	anc2r 539	Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
|- ((ph -> (ps -> ch)) -> (ph -> (ps -> (ch /\ ph))))
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.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ph /\ ch)))
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.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ch /\ ph)))
Theorem	pm3.41 542	Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> ch) -> ((ph /\ ps) -> ch))
Theorem	pm3.42 543	Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
|- ((ps -> ch) -> ((ph /\ ps) -> ch))
Theorem	pm3.4 544	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
|- ((ph /\ ps) -> (ph -> ps))
Theorem	pm4.45im 545	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
|- (ph <-> (ph /\ (ps -> ph)))
Theorem	anim12d 546	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta))   =>   |- (ph -> ((ps /\ th) -> (ch /\ ta)))
Theorem	anim1d 547	Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
|- (ph -> (ps -> ch))   =>   |- (ph -> ((ps /\ th) -> (ch /\ th)))
Theorem	anim2d 548	Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps -> ch))   =>   |- (ph -> ((th /\ ps) -> (th /\ ch)))
Theorem	anim12i 549	Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph /\ ch) -> (ps /\ th))
Theorem	anim12ci 550	Variant of anim12i 549 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph /\ ch) -> (th /\ ps))
Theorem	anim1i 551	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ps)   =>   |- ((ph /\ ch) -> (ps /\ ch))
Theorem	anim2i 552	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ps)   =>   |- ((ch /\ ph) -> (ch /\ ps))
Theorem	anim12ii 553	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.)
|- (ph -> (ps -> ch))   &   |- (th -> (ps -> ta))   =>   |- ((ph /\ th) -> (ps -> (ch /\ ta)))
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.)
|- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))
Theorem	pm2.3 555	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
|- ((ph \/ (ps \/ ch)) -> (ph \/ (ch \/ ps)))
Theorem	pm2.41 556	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ((ps \/ (ph \/ ps)) -> (ph \/ ps))
Theorem	pm2.42 557	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ((-. ph \/ (ph -> ps)) -> (ph -> ps))
Theorem	pm2.4 558	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
|- ((ph \/ (ph \/ ps)) -> (ph \/ ps))
Theorem	pm2.65da 559	Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ps) -> -. ch)   =>   |- (ph -> -. ps)
Theorem	pm4.44 560	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
|- (ph <-> (ph \/ (ph /\ ps)))
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.)
|- (((ph /\ ps) -> ch) <-> ((ph /\ -. ch) -> -. ps))
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.)
|- (((ph /\ ps) -> ch) -> ((ph /\ -. ch) -> -. ps))
Theorem	nan 563	Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.)
|- ((ph -> -. (ps /\ ch)) <-> ((ph /\ ps) -> -. ch))
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.)
|- (((ph /\ ps) -> -. ch) <-> ((ps /\ ch) -> -. ph))
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.)
|- (((ph -> ps) \/ (ph -> ch)) <-> (ph -> (ps \/ ch)))
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.)
|- (((ps -> ph) \/ (ch -> ph)) <-> ((ps /\ ch) -> ph))
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.)
|- (((((ph /\ ps) -> ch) <-> (ph -> (ps -> ch))) /\ ((ph -> (ps -> ch)) <-> (ps -> (ph -> ch)))) /\ ((ps -> (ph -> ch)) <-> ((ps /\ ph) -> ch)))
Theorem	pm3.33 568	Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
|- (((ph -> ps) /\ (ps -> ch)) -> (ph -> ch))
Theorem	pm3.34 569	Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
|- (((ps -> ch) /\ (ph -> ps)) -> (ph -> ch))
Theorem	pm3.35 570	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
|- ((ph /\ (ph -> ps)) -> ps)
Theorem	pm5.31 571	Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ((ch /\ (ph -> ps)) -> (ph -> (ps /\ ch)))
Theorem	imp4a 572	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ph -> (ps -> ((ch /\ th) -> ta)))
Theorem	imp4b 573	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- ((ph /\ ps) -> ((ch /\ th) -> ta))
Theorem	imp4c 574	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ph -> (((ps /\ ch) /\ th) -> ta))
Theorem	imp4d 575	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ph -> ((ps /\ (ch /\ th)) -> ta))
Theorem	imp41 576	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- ((((ph /\ ps) /\ ch) /\ th) -> ta)
Theorem	imp42 577	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (((ph /\ (ps /\ ch)) /\ th) -> ta)
Theorem	imp43 578	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
Theorem	imp44 579	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- ((ph /\ ((ps /\ ch) /\ th)) -> ta)
Theorem	imp45 580	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- ((ph /\ (ps /\ (ch /\ th))) -> ta)
Theorem	imp5a 581	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- (ph -> (ps -> (ch -> (th -> (ta -> et)))))   =>   |- (ph -> (ps -> (ch -> ((th /\ ta) -> et))))
Theorem	imp5d 582	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- (ph -> (ps -> (ch -> (th -> (ta -> et)))))   =>   |- (((ph /\ ps) /\ ch) -> ((th /\ ta) -> et))
Theorem	imp5g 583	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- (ph -> (ps -> (ch -> (th -> (ta -> et)))))   =>   |- ((ph /\ ps) -> (((ch /\ th) /\ ta) -> et))
Theorem	imp55 584	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- (ph -> (ps -> (ch -> (th -> (ta -> et)))))   =>   |- (((ph /\ (ps /\ (ch /\ th))) /\ ta) -> et)
Theorem	imp511 585	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- (ph -> (ps -> (ch -> (th -> (ta -> et)))))   =>   |- ((ph /\ ((ps /\ (ch /\ th)) /\ ta)) -> et)
Theorem	expimpd 586	Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
|- ((ph /\ ps) -> (ch -> th))   =>   |- (ph -> ((ps /\ ch) -> th))
Theorem	exp31 587	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- (((ph /\ ps) /\ ch) -> th)   =>   |- (ph -> (ps -> (ch -> th)))
Theorem	exp32 588	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ((ph /\ (ps /\ ch)) -> th)   =>   |- (ph -> (ps -> (ch -> th)))
Theorem	exp4a 589	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> ((ch /\ th) -> ta)))   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	exp4b 590	An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
|- ((ph /\ ps) -> ((ch /\ th) -> ta))   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	exp4c 591	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (((ps /\ ch) /\ th) -> ta))   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	exp4d 592	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> ((ps /\ (ch /\ th)) -> ta))   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	exp41 593	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ((((ph /\ ps) /\ ch) /\ th) -> ta)   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	exp42 594	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- (((ph /\ (ps /\ ch)) /\ th) -> ta)   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	exp43 595	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- (((ph /\ ps) /\ (ch /\ th)) -> ta)   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	exp44 596	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ((ph /\ ((ps /\ ch) /\ th)) -> ta)   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	exp45 597	An exportation inference. (Contributed by NM, 26-Apr-1994.)
|- ((ph /\ (ps /\ (ch /\ th))) -> ta)   =>   |- (ph -> (ps -> (ch -> (th -> ta))))
Theorem	expr 598	Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ ps) -> (ch -> th))
Theorem	exp5c 599	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- (ph -> ((ps /\ ch) -> ((th /\ ta) -> et)))   =>   |- (ph -> (ps -> (ch -> (th -> (ta -> et)))))
Theorem	exp53 600	An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
|- ((((ph /\ ps) /\ (ch /\ th)) /\ ta) -> et)   =>   |- (ph -> (ps -> (ch -> (th -> (ta -> et)))))