Theorem 3imp21 1113

Description: The importation inference 3imp 1110 with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) (Revised to shorten 3com12 1123 by Wolf Lammen, 23-Jun-2022.)

Hypothesis

Ref	Expression
3imp.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
3imp21	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem 3imp21

Step	Hyp	Ref	Expression
1		3imp.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com13 88	. 2 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))
3	2	3imp231 1112	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  3com12  1123  sotri3  6087  isinf  9165  infssuni  9246  fin1a2lem10  10319  elfz1b  13509  bernneq  14152  expnngt1  14164  swrdco  14760  dfgcd2  16473  lmodvsmmulgdi  20848  mamufacex  22340  gausslemma2dlem1a  27332  sltsun1  27784  sltsright  27857  expsgt0  28433  bdaypw2n0bnd  28460  upgrewlkle2  29680  pthdivtx  29800  clwwlkinwwlk  30115  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  numclwwlk2lem1lem  30417  frgrregord013  30470  ax6e2ndeqALT  45171  fmtnofac2  47815