Theorem 3imp21 1112

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3com12  1121  sotri3  6024  isinf  8965  infssuni  9040  fin1a2lem10  10096  elfz1b  13254  bernneq  13872  expnngt1  13884  swrdco  14478  dfgcd2  16182  lmodvsmmulgdi  20073  mamufacex  21448  gausslemma2dlem1a  26418  upgrewlkle2  27876  pthdivtx  27998  clwwlkinwwlk  28305  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  numclwwlk2lem1lem  28607  frgrregord013  28660  ssltun1  33929  ssltright  33982  ax6e2ndeqALT  42440  fmtnofac2  44909