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  6093  isinf  9175  infssuni  9256  fin1a2lem10  10331  elfz1b  13547  bernneq  14191  expnngt1  14203  swrdco  14799  dfgcd2  16515  lmodvsmmulgdi  20892  mamufacex  22361  gausslemma2dlem1a  27328  sltsun1  27780  sltsright  27853  expsgt0  28429  bdaypw2n0bnd  28456  upgrewlkle2  29675  pthdivtx  29795  clwwlkinwwlk  30110  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  numclwwlk2lem1lem  30412  frgrregord013  30465  ax6e2ndeqALT  45357  nnmul2  47778  fmtnofac2  48032