Theorem 3imp21 1126

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

Syntax hints:   → wi 4   ∧ w3a 1098

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

This theorem is referenced by:  3com12  1136  sotri3  6117  isinf  9209  infssuni  9289  fin1a2lem10  10366  elfz1b  13598  bernneq  14242  expnngt1  14254  swrdco  14850  dfgcd2  16580  lmodvsmmulgdi  20961  mamufacex  22453  gausslemma2dlem1a  27426  sltsun1  27878  sltsright  27951  expsgt0  28527  bdaypw2n0bnd  28554  upgrewlkle2  29804  pthdivtx  29924  clwwlkinwwlk  30239  upgr3v3e3cycl  30379  upgr4cycl4dv4e  30384  numclwwlk2lem1lem  30541  frgrregord013  30594  ax6e2ndeqALT  45503  nnmul2  47921  fmtnofac2  48175