P. 4 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 301-400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	biantrur 301	A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))
Theorem	biantrud 302	A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))
Theorem	biantrurd 303	A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
Theorem	jca 304	Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jcad 305	Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	jca2 306	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	jca31 307	Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
Theorem	jca32 308	Join three consequents. (Contributed by FL, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
Theorem	jcai 309	Deduction replacing implication with conjunction. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jctil 310	Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓))
Theorem	jctir 311	Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jctl 312	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 313	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 314	Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jctird 315	Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	ancl 316	Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜑 ∧ 𝜓)))
Theorem	anclb 317	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 318	Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))))
Theorem	ancr 319	Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜓 ∧ 𝜑)))
Theorem	ancrb 320	Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ∧ 𝜑)))
Theorem	ancli 321	Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜑 ∧ 𝜓))
Theorem	ancri 322	Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜑))
Theorem	ancld 323	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 324	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 325	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 326	Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜒 ∧ 𝜑))))
Theorem	anc2li 327	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 328	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 329	Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	pm3.42 330	Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	pm3.4 331	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓))
Theorem	pm4.45im 332	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜓 → 𝜑)))
Theorem	anim12d 333	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
Theorem	anim1d 334	Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))
Theorem	anim2d 335	Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))
Theorem	anim12i 336	Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))
Theorem	anim12ci 337	Variant of anim12i 336 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))
Theorem	anim1i 338	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
Theorem	anim1ci 339	Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓))
Theorem	anim2i 340	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))
Theorem	anim12ii 341	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜓 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → (𝜒 ∧ 𝜏)))
Theorem	anim12 342	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	pm3.33 343	Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜒)) → (𝜑 → 𝜒))
Theorem	pm3.34 344	Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜓 → 𝜒) ∧ (𝜑 → 𝜓)) → (𝜑 → 𝜒))
Theorem	pm3.35 345	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)
Theorem	pm5.31 346	Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜒 ∧ (𝜑 → 𝜓)) → (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	imp4a 347	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))
Theorem	imp4b 348	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
Theorem	imp4c 349	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))
Theorem	imp4d 350	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏))
Theorem	imp41 351	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	imp42 352	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)
Theorem	imp43 353	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
Theorem	imp44 354	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏)
Theorem	imp45 355	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜏)
Theorem	imp5a 356	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → ((𝜃 ∧ 𝜏) → 𝜂))))
Theorem	imp5d 357	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))
Theorem	imp5g 358	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (((𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂))
Theorem	imp55 359	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ∧ 𝜏) → 𝜂)
Theorem	imp511 360	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏)) → 𝜂)
Theorem	expimpd 361	Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	exp31 362	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	exp32 363	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	exp4a 364	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4b 365	An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4c 366	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4d 367	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp41 368	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp42 369	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp43 370	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp44 371	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp45 372	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	expr 373	Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	exp5c 374	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp53 375	An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	expl 376	Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	impr 377	Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	impl 378	Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	impac 379	Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜓))
Theorem	exbiri 380	Inference form of exbir 1429. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
Theorem	simprbda 381	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	simplbda 382	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	simplbi2 383	Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜑))
Theorem	simpl2im 384	Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	simplbiim 385	Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	dfbi2 386	A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
Theorem	pm4.71 387	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓)))
Theorem	pm4.71r 388	Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
Theorem	pm4.71i 389	Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
Theorem	pm4.71ri 390	Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))
Theorem	pm4.71d 391	Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
Theorem	pm4.71rd 392	Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))
Theorem	pm4.24 393	Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 14-Mar-2014.)
⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
Theorem	anidm 394	Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)
Theorem	anidms 395	Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
⊢ ((𝜑 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	anidmdbi 396	Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
⊢ ((𝜑 → (𝜓 ∧ 𝜓)) ↔ (𝜑 → 𝜓))
Theorem	anasss 397	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	anassrs 398	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	anass 399	Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	sylanl1 400	A syllogism inference. (Contributed by NM, 10-Mar-2005.)
⊢ (𝜑 → 𝜓)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)