Theorem 3imp21 1110

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3com12  1119  sotri3  5990  isinf  8731  infssuni  8815  fin1a2lem10  9831  elfz1b  12977  bernneq  13591  expnngt1  13603  swrdco  14199  dfgcd2  15894  lmodvsmmulgdi  19669  mamufacex  21000  gausslemma2dlem1a  25941  upgrewlkle2  27388  pthdivtx  27510  clwwlkinwwlk  27818  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  numclwwlk2lem1lem  28121  frgrregord013  28174  ax6e2ndeqALT  41285  fmtnofac2  43751