Theorem impcomd 411

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 410	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  sbequ2  2244  sbequ2OLD  2245  ralxfrd  5326  ralxfrd2  5330  iss  5932  dfpo2  6188  funssres  6462  fv3  6774  fmptsnd  7023  frrlem10  8082  wfr3g  8109  nnmord  8425  cfcoflem  9959  nqereu  10616  ltletr  10997  fzind  12348  eqreznegel  12603  xrltletr  12820  xnn0xaddcl  12898  elfzodifsumelfzo  13381  hash2prde  14112  fundmge2nop0  14134  wrd2ind  14364  swrdccatin1  14366  rlimuni  15187  rlimno1  15293  ndvdssub  16046  lcmfunsnlem2  16273  coprmdvds  16286  coprmdvds2  16287  gsmsymgrfixlem1  18950  lsmdisj2  19203  chfacfisf  21911  chfacfisfcpmat  21912  lmcnp  22363  1stccnp  22521  txlm  22707  fgss2  22933  fgfil  22934  ufileu  22978  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  ufilcmp  23091  cnpfcf  23100  alexsubALTlem2  23107  tsmsxp  23214  ivthlem2  24521  ivthlem3  24522  2sqreultlem  26500  2sqreultblem  26501  2sqreunnltlem  26503  2sqreunnltblem  26504  umgrislfupgrlem  27395  uhgr2edg  27478  wlkv0  27920  usgr2pth  28033  clwlkclwwlklem2  28265  frgrregord013  28660  prsrcmpltd  32955  sat1el2xp  33241  goalrlem  33258