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  2254  ralxfrd  5348  ralxfrd2  5352  iss  5988  dfpo2  6248  funssres  6530  fv3  6846  fmptsnd  7109  resf1extb  7870  frrlem10  8231  wfr3g  8255  nnmord  8553  cfcoflem  10170  nqereu  10827  ltletr  11212  fzind  12577  eqreznegel  12834  xrltletr  13058  xnn0xaddcl  13136  elfzodifsumelfzo  13633  hash2prde  14379  hash3tpde  14402  fundmge2nop0  14411  wrd2ind  14632  swrdccatin1  14634  rlimuni  15459  rlimno1  15563  ndvdssub  16322  lcmfunsnlem2  16553  coprmdvds  16566  coprmdvds2  16567  gsmsymgrfixlem1  19341  lsmdisj2  19596  chfacfisf  22770  chfacfisfcpmat  22771  lmcnp  23220  1stccnp  23378  txlm  23564  fgss2  23790  fgfil  23791  ufileu  23835  rnelfm  23869  fmfnfmlem2  23871  fmfnfmlem4  23873  ufilcmp  23948  cnpfcf  23957  alexsubALTlem2  23964  tsmsxp  24071  ivthlem2  25381  ivthlem3  25382  2sqreultlem  27386  2sqreultblem  27387  2sqreunnltlem  27389  2sqreunnltblem  27390  negsid  27984  bdayon  28210  umgrislfupgrlem  29102  uhgr2edg  29188  wlkv0  29630  usgr2pth  29744  clwlkclwwlklem2  29982  frgrregord013  30377  prsrcmpltd  35114  r1filimi  35135  sat1el2xp  35444  goalrlem  35461  uhgrimedgi  48014  isubgr3stgrlem7  48096  grlimgrtri  48127  pgnbgreunbgrlem2  48241  pgnbgreunbgrlem5  48247