Theorem 3imp21 1115

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3com12  1124  sotri3  6132  isinf  9260  isinfOLD  9261  infssuni  9343  fin1a2lem10  10404  elfz1b  13570  bernneq  14192  expnngt1  14204  swrdco  14788  dfgcd2  16488  lmodvsmmulgdi  20507  mamufacex  21891  gausslemma2dlem1a  26868  ssltun1  27309  ssltright  27366  upgrewlkle2  28863  pthdivtx  28986  clwwlkinwwlk  29293  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  numclwwlk2lem1lem  29595  frgrregord013  29648  ax6e2ndeqALT  43692  fmtnofac2  46237