Theorem 3imp21 1119

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3com12  1129  sotri3  6080  isinf  9165  infssuni  9246  fin1a2lem10  10322  elfz1b  13538  bernneq  14182  expnngt1  14194  swrdco  14790  dfgcd2  16506  lmodvsmmulgdi  20887  mamufacex  22379  gausslemma2dlem1a  27346  sltsun1  27798  sltsright  27871  expsgt0  28447  bdaypw2n0bnd  28474  upgrewlkle2  29693  pthdivtx  29813  clwwlkinwwlk  30128  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  numclwwlk2lem1lem  30430  frgrregord013  30483  ax6e2ndeqALT  45374  nnmul2  47793  fmtnofac2  48047