Theorem 3imp21 1111

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  3com12  1120  sotri3  5957  isinf  8715  infssuni  8799  fin1a2lem10  9820  elfz1b  12971  bernneq  13586  expnngt1  13598  swrdco  14190  dfgcd2  15884  lmodvsmmulgdi  19662  mamufacex  20996  gausslemma2dlem1a  25949  upgrewlkle2  27396  pthdivtx  27518  clwwlkinwwlk  27825  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  numclwwlk2lem1lem  28127  frgrregord013  28180  ax6e2ndeqALT  41637  fmtnofac2  44086