Theorem 3imp21 1114

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3com12  1124  sotri3  6088  isinf  9169  infssuni  9250  fin1a2lem10  10325  elfz1b  13541  bernneq  14185  expnngt1  14197  swrdco  14793  dfgcd2  16509  lmodvsmmulgdi  20886  mamufacex  22374  gausslemma2dlem1a  27345  sltsun1  27797  sltsright  27870  expsgt0  28446  bdaypw2n0bnd  28473  upgrewlkle2  29693  pthdivtx  29813  clwwlkinwwlk  30128  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  numclwwlk2lem1lem  30430  frgrregord013  30483  ax6e2ndeqALT  45378  nnmul2  47793  fmtnofac2  48047