Theorem 3imp21 1142

Description: The importation inference 3imp 1138 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 1154 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 1141	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  3com12  1154  sotri3  5742  elfz1b  12659  expnngt1  13278  gausslemma2dlem1a  25439  upgrewlkle2  26848  pthdivtx  26975  clwwlkinwwlk  27340  clwwlkinwwlkOLD  27341  clwlksfclwwlkOLD  27395  upgr3v3e3cycl  27516  upgr4cycl4dv4e  27521  numclwwlk2lem1lem  27684  frgrregord013  27772  ax6e2ndeqALT  39915  fmtnofac2  42251