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  5363  ralxfrd2  5367  iss  6006  dfpo2  6269  funssres  6560  fv3  6876  fmptsnd  7143  resf1extb  7910  frrlem10  8274  wfr3g  8298  nnmord  8596  cfcoflem  10225  nqereu  10882  ltletr  11266  fzind  12632  eqreznegel  12893  xrltletr  13117  xnn0xaddcl  13195  elfzodifsumelfzo  13692  hash2prde  14435  hash3tpde  14458  fundmge2nop0  14467  wrd2ind  14688  swrdccatin1  14690  rlimuni  15516  rlimno1  15620  ndvdssub  16379  lcmfunsnlem2  16610  coprmdvds  16623  coprmdvds2  16624  gsmsymgrfixlem1  19357  lsmdisj2  19612  chfacfisf  22741  chfacfisfcpmat  22742  lmcnp  23191  1stccnp  23349  txlm  23535  fgss2  23761  fgfil  23762  ufileu  23806  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  ufilcmp  23919  cnpfcf  23928  alexsubALTlem2  23935  tsmsxp  24042  ivthlem2  25353  ivthlem3  25354  2sqreultlem  27358  2sqreultblem  27359  2sqreunnltlem  27361  2sqreunnltblem  27362  negsid  27947  bdayon  28173  umgrislfupgrlem  29049  uhgr2edg  29135  wlkv0  29579  usgr2pth  29694  clwlkclwwlklem2  29929  frgrregord013  30324  prsrcmpltd  35071  sat1el2xp  35366  goalrlem  35383  uhgrimedgi  47890  isubgr3stgrlem7  47971  grlimgrtri  47995  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem5  48113