Theorem 3imp21 1131

Description: The importation inference 3imp 1128 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 1141 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 89	. 2 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))
3	2	3imp231 1130	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3com12  1141  sotri3  6142  isinf  9294  infssuni  9373  fin1a2lem10  10526  elfz1b  13767  bernneq  14414  expnngt1  14426  swrdco  15030  dfgcd2  16763  lmodvsmmulgdi  21223  mamufacex  22766  gausslemma2dlem1a  27749  sltsun1  28231  sltsright  28304  expsgt0  28880  bdaypw2n0bnd  28907  upgrewlkle2  30244  pthdivtx  30369  clwwlkinwwlk  30688  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  numclwwlk2lem1lem  31000  frgrregord013  31053  elpssmo  36673  ax6e2ndeqALT  46173  nnmul2  48673  fmtnofac2  48927