Theorem 3imp21 1129

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  3com12  1139  sotri3  6131  isinf  9224  infssuni  9302  fin1a2lem10  10392  elfz1b  13620  bernneq  14264  expnngt1  14276  swrdco  14873  dfgcd2  16603  lmodvsmmulgdi  20995  mamufacex  22521  gausslemma2dlem1a  27494  sltsun1  27946  sltsright  28019  expsgt0  28595  bdaypw2n0bnd  28622  upgrewlkle2  29896  pthdivtx  30016  clwwlkinwwlk  30331  upgr3v3e3cycl  30471  upgr4cycl4dv4e  30476  numclwwlk2lem1lem  30633  frgrregord013  30686  ax6e2ndeqALT  45530  nnmul2  47955  fmtnofac2  48209