Theorem 3imp21 1114

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3com12  1123  sotri3  6162  isinf  9323  isinfOLD  9324  infssuni  9414  fin1a2lem10  10478  elfz1b  13653  bernneq  14278  expnngt1  14290  swrdco  14886  dfgcd2  16593  lmodvsmmulgdi  20917  mamufacex  22421  gausslemma2dlem1a  27427  ssltun1  27871  ssltright  27928  expsgt0  28433  upgrewlkle2  29642  pthdivtx  29765  clwwlkinwwlk  30072  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  numclwwlk2lem1lem  30374  frgrregord013  30427  ax6e2ndeqALT  44902  fmtnofac2  47443