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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3com12  1141  sotri3  6124  isinf  9249  infssuni  9328  fin1a2lem10  10480  elfz1b  13720  bernneq  14366  expnngt1  14378  swrdco  14981  dfgcd2  16712  lmodvsmmulgdi  21165  mamufacex  22704  gausslemma2dlem1a  27685  sltsun1  28167  sltsright  28240  expsgt0  28816  bdaypw2n0bnd  28843  upgrewlkle2  30180  pthdivtx  30305  clwwlkinwwlk  30624  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  numclwwlk2lem1lem  30936  frgrregord013  30989  ax6e2ndeqALT  45898  nnmul2  48369  fmtnofac2  48623