Theorem impcomd 412

Description: Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.)

Hypothesis

Ref	Expression
impd.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
impcomd	⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Proof of Theorem impcomd

Step	Hyp	Ref	Expression
1		impd.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com23 86	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	impd 411	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 396

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

This theorem is referenced by:  sbequ2  2240  sbequ2OLD  2241  ralxfrd  5344  ralxfrd2  5348  iss  5960  dfpo2  6219  funssres  6512  fv3  6827  fmptsnd  7078  frrlem10  8156  wfr3g  8183  nnmord  8509  cfcoflem  10098  nqereu  10755  ltletr  11137  fzind  12488  eqreznegel  12744  xrltletr  12961  xnn0xaddcl  13039  elfzodifsumelfzo  13523  hash2prde  14253  fundmge2nop0  14275  wrd2ind  14505  swrdccatin1  14507  rlimuni  15328  rlimno1  15434  ndvdssub  16187  lcmfunsnlem2  16412  coprmdvds  16425  coprmdvds2  16426  gsmsymgrfixlem1  19102  lsmdisj2  19355  chfacfisf  22074  chfacfisfcpmat  22075  lmcnp  22526  1stccnp  22684  txlm  22870  fgss2  23096  fgfil  23097  ufileu  23141  rnelfm  23175  fmfnfmlem2  23177  fmfnfmlem4  23179  ufilcmp  23254  cnpfcf  23263  alexsubALTlem2  23270  tsmsxp  23377  ivthlem2  24687  ivthlem3  24688  2sqreultlem  26666  2sqreultblem  26667  2sqreunnltlem  26669  2sqreunnltblem  26670  umgrislfupgrlem  27600  uhgr2edg  27683  wlkv0  28126  usgr2pth  28240  clwlkclwwlklem2  28472  frgrregord013  28867  prsrcmpltd  33161  sat1el2xp  33447  goalrlem  33464