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  2257  ralxfrd  5355  ralxfrd2  5359  iss  6002  dfpo2  6262  funssres  6544  fv3  6860  fmptsnd  7125  resf1extb  7886  frrlem10  8247  wfr3g  8271  nnmord  8570  cfcoflem  10194  nqereu  10852  ltletr  11237  fzind  12602  eqreznegel  12859  xrltletr  13083  xnn0xaddcl  13162  elfzodifsumelfzo  13659  hash2prde  14405  hash3tpde  14428  fundmge2nop0  14437  wrd2ind  14658  swrdccatin1  14660  rlimuni  15485  rlimno1  15589  ndvdssub  16348  lcmfunsnlem2  16579  coprmdvds  16592  coprmdvds2  16593  gsmsymgrfixlem1  19368  lsmdisj2  19623  chfacfisf  22810  chfacfisfcpmat  22811  lmcnp  23260  1stccnp  23418  txlm  23604  fgss2  23830  fgfil  23831  ufileu  23875  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem4  23913  ufilcmp  23988  cnpfcf  23997  alexsubALTlem2  24004  tsmsxp  24111  ivthlem2  25421  ivthlem3  25422  2sqreultlem  27426  2sqreultblem  27427  2sqreunnltlem  27429  2sqreunnltblem  27430  negsid  28049  bdayons  28284  z12bdaylem  28492  umgrislfupgrlem  29207  uhgr2edg  29293  wlkv0  29735  usgr2pth  29849  clwlkclwwlklem2  30087  frgrregord013  30482  prsrcmpltd  35256  r1filimi  35278  sat1el2xp  35592  goalrlem  35609  uhgrimedgi  48244  isubgr3stgrlem7  48326  grlimgrtri  48357  pgnbgreunbgrlem2  48471  pgnbgreunbgrlem5  48477