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  2241  sbequ2OLD  2242  ralxfrd  5331  ralxfrd2  5335  iss  5943  dfpo2  6199  funssres  6478  fv3  6792  fmptsnd  7041  frrlem10  8111  wfr3g  8138  nnmord  8463  cfcoflem  10028  nqereu  10685  ltletr  11067  fzind  12418  eqreznegel  12674  xrltletr  12891  xnn0xaddcl  12969  elfzodifsumelfzo  13453  hash2prde  14184  fundmge2nop0  14206  wrd2ind  14436  swrdccatin1  14438  rlimuni  15259  rlimno1  15365  ndvdssub  16118  lcmfunsnlem2  16345  coprmdvds  16358  coprmdvds2  16359  gsmsymgrfixlem1  19035  lsmdisj2  19288  chfacfisf  22003  chfacfisfcpmat  22004  lmcnp  22455  1stccnp  22613  txlm  22799  fgss2  23025  fgfil  23026  ufileu  23070  rnelfm  23104  fmfnfmlem2  23106  fmfnfmlem4  23108  ufilcmp  23183  cnpfcf  23192  alexsubALTlem2  23199  tsmsxp  23306  ivthlem2  24616  ivthlem3  24617  2sqreultlem  26595  2sqreultblem  26596  2sqreunnltlem  26598  2sqreunnltblem  26599  umgrislfupgrlem  27492  uhgr2edg  27575  wlkv0  28018  usgr2pth  28132  clwlkclwwlklem2  28364  frgrregord013  28759  prsrcmpltd  33055  sat1el2xp  33341  goalrlem  33358