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 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3com12  1141  sotri3  6130  isinf  9221  infssuni  9299  fin1a2lem10  10388  elfz1b  13617  bernneq  14261  expnngt1  14273  swrdco  14870  dfgcd2  16599  lmodvsmmulgdi  21018  mamufacex  22553  gausslemma2dlem1a  27529  sltsun1  27981  sltsright  28054  expsgt0  28630  bdaypw2n0bnd  28657  upgrewlkle2  29956  pthdivtx  30076  clwwlkinwwlk  30391  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  numclwwlk2lem1lem  30693  frgrregord013  30746  ax6e2ndeqALT  45639  nnmul2  48067  fmtnofac2  48321