Theorem 3imp21 1111

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  3com12  1120  sotri3  6141  isinf  9291  isinfOLD  9292  infssuni  9375  fin1a2lem10  10440  elfz1b  13610  bernneq  14231  expnngt1  14243  swrdco  14828  dfgcd2  16529  lmodvsmmulgdi  20787  mamufacex  22311  gausslemma2dlem1a  27318  ssltun1  27761  ssltright  27818  upgrewlkle2  29440  pthdivtx  29563  clwwlkinwwlk  29870  upgr3v3e3cycl  30010  upgr4cycl4dv4e  30015  numclwwlk2lem1lem  30172  frgrregord013  30225  ax6e2ndeqALT  44401  fmtnofac2  46938