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  2250  ralxfrd  5366  ralxfrd2  5370  iss  6009  dfpo2  6272  funssres  6563  fv3  6879  fmptsnd  7146  resf1extb  7913  frrlem10  8277  wfr3g  8301  nnmord  8599  cfcoflem  10232  nqereu  10889  ltletr  11273  fzind  12639  eqreznegel  12900  xrltletr  13124  xnn0xaddcl  13202  elfzodifsumelfzo  13699  hash2prde  14442  hash3tpde  14465  fundmge2nop0  14474  wrd2ind  14695  swrdccatin1  14697  rlimuni  15523  rlimno1  15627  ndvdssub  16386  lcmfunsnlem2  16617  coprmdvds  16630  coprmdvds2  16631  gsmsymgrfixlem1  19364  lsmdisj2  19619  chfacfisf  22748  chfacfisfcpmat  22749  lmcnp  23198  1stccnp  23356  txlm  23542  fgss2  23768  fgfil  23769  ufileu  23813  rnelfm  23847  fmfnfmlem2  23849  fmfnfmlem4  23851  ufilcmp  23926  cnpfcf  23935  alexsubALTlem2  23942  tsmsxp  24049  ivthlem2  25360  ivthlem3  25361  2sqreultlem  27365  2sqreultblem  27366  2sqreunnltlem  27368  2sqreunnltblem  27369  negsid  27954  bdayon  28180  umgrislfupgrlem  29056  uhgr2edg  29142  wlkv0  29586  usgr2pth  29701  clwlkclwwlklem2  29936  frgrregord013  30331  prsrcmpltd  35078  sat1el2xp  35373  goalrlem  35390  uhgrimedgi  47894  isubgr3stgrlem7  47975  grlimgrtri  47999  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem5  48117