Theorem 3imp21 1113

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

Syntax hints:   → wi 4   ∧ w3a 1086

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

This theorem is referenced by:  3com12  1122  sotri3  6035  isinf  9036  infssuni  9110  fin1a2lem10  10165  elfz1b  13325  bernneq  13944  expnngt1  13956  swrdco  14550  dfgcd2  16254  lmodvsmmulgdi  20158  mamufacex  21538  gausslemma2dlem1a  26513  upgrewlkle2  27973  pthdivtx  28097  clwwlkinwwlk  28404  upgr3v3e3cycl  28544  upgr4cycl4dv4e  28549  numclwwlk2lem1lem  28706  frgrregord013  28759  ssltun1  34002  ssltright  34055  ax6e2ndeqALT  42551  fmtnofac2  45021