Theorem 3imp21 1131

Description: The importation inference 3imp 1128 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 1141 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 89	. 2 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))
3	2	3imp231 1130	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3com12  1141  sotri3  6124  isinf  9235  infssuni  9313  fin1a2lem10  10411  elfz1b  13648  bernneq  14293  expnngt1  14305  swrdco  14908  dfgcd2  16636  lmodvsmmulgdi  21081  mamufacex  22618  gausslemma2dlem1a  27601  sltsun1  28053  sltsright  28126  expsgt0  28702  bdaypw2n0bnd  28729  upgrewlkle2  30066  pthdivtx  30191  clwwlkinwwlk  30510  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  numclwwlk2lem1lem  30822  frgrregord013  30875  ax6e2ndeqALT  45753  nnmul2  48218  fmtnofac2  48472