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 207  df-an 396

This theorem is referenced by:  sbequ2  2246  ralxfrd  5413  ralxfrd2  5417  iss  6054  dfpo2  6317  funssres  6611  fv3  6924  fmptsnd  7188  frrlem10  8318  wfr3g  8345  nnmord  8668  cfcoflem  10309  nqereu  10966  ltletr  11350  fzind  12713  eqreznegel  12973  xrltletr  13195  xnn0xaddcl  13273  elfzodifsumelfzo  13766  hash2prde  14505  hash3tpde  14528  fundmge2nop0  14537  wrd2ind  14757  swrdccatin1  14759  rlimuni  15582  rlimno1  15686  ndvdssub  16442  lcmfunsnlem2  16673  coprmdvds  16686  coprmdvds2  16687  gsmsymgrfixlem1  19459  lsmdisj2  19714  chfacfisf  22875  chfacfisfcpmat  22876  lmcnp  23327  1stccnp  23485  txlm  23671  fgss2  23897  fgfil  23898  ufileu  23942  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem4  23980  ufilcmp  24055  cnpfcf  24064  alexsubALTlem2  24071  tsmsxp  24178  ivthlem2  25500  ivthlem3  25501  2sqreultlem  27505  2sqreultblem  27506  2sqreunnltlem  27508  2sqreunnltblem  27509  negsid  28087  umgrislfupgrlem  29153  uhgr2edg  29239  wlkv0  29683  usgr2pth  29796  clwlkclwwlklem2  30028  frgrregord013  30423  prsrcmpltd  35073  sat1el2xp  35363  goalrlem  35380  isubgr3stgrlem7  47874  grlimgrtri  47898