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  6132  isinf  9232  infssuni  9310  fin1a2lem10  10408  elfz1b  13638  bernneq  14283  expnngt1  14295  swrdco  14898  dfgcd2  16626  lmodvsmmulgdi  21068  mamufacex  22603  gausslemma2dlem1a  27580  sltsun1  28032  sltsright  28105  expsgt0  28681  bdaypw2n0bnd  28708  upgrewlkle2  30014  pthdivtx  30139  clwwlkinwwlk  30458  upgr3v3e3cycl  30602  upgr4cycl4dv4e  30607  numclwwlk2lem1lem  30764  frgrregord013  30817  ax6e2ndeqALT  45697  nnmul2  48125  fmtnofac2  48379