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  6126  isinf  9263  infssuni  9342  fin1a2lem10  10494  elfz1b  13734  bernneq  14380  expnngt1  14392  swrdco  14996  dfgcd2  16728  lmodvsmmulgdi  21181  mamufacex  22720  gausslemma2dlem1a  27701  sltsun1  28183  sltsright  28256  expsgt0  28832  bdaypw2n0bnd  28859  upgrewlkle2  30196  pthdivtx  30321  clwwlkinwwlk  30640  upgr3v3e3cycl  30790  upgr4cycl4dv4e  30795  numclwwlk2lem1lem  30952  frgrregord013  31005  ax6e2ndeqALT  46021  nnmul2  48508  fmtnofac2  48762