Theorem impcomd 416

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 87	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	impd 415	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sbequ2  2291  ralxfrd  5377  ralxfrd2  5381  iss  6035  dfpo2  6295  funssres  6578  fv3  6897  fmptsnd  7165  resf1extb  7927  frrlem10  8288  wfr3g  8312  nnmord  8614  elirrv  9555  cfcoflem  10252  nqereu  10910  ltletr  11298  fzind  12690  eqreznegel  12954  xrltletr  13178  xnn0xaddcl  13257  elfzodifsumelfzo  13756  hash2prde  14503  hash3tpde  14526  fundmge2nop0  14535  wrd2ind  14756  swrdccatin1  14758  rlimuni  15597  rlimno1  15701  ndvdssub  16463  lcmfunsnlem2  16694  coprmdvds  16707  coprmdvds2  16708  gsmsymgrfixlem1  19493  lsmdisj2  19748  chfacfisf  22976  chfacfisfcpmat  22977  lmcnp  23426  1stccnp  23584  txlm  23770  fgss2  23996  fgfil  23997  ufileu  24041  rnelfm  24075  fmfnfmlem2  24077  fmfnfmlem4  24079  ufilcmp  24154  cnpfcf  24163  alexsubALTlem2  24170  tsmsxp  24277  ivthlem2  25576  ivthlem3  25577  2sqreultlem  27573  2sqreultblem  27574  2sqreunnltlem  27576  2sqreunnltblem  27577  negsid  28196  bdayons  28431  z12bdaylem  28639  umgrislfupgrlem  29409  uhgr2edg  29495  wlkv0  29936  usgr2pth  30050  clwlkclwwlklem2  30288  frgrregord013  30683  prsrcmpltd  35410  r1filimi  35435  sat1el2xp  35766  goalrlem  35783  axuntco  36875  uhgrimedgi  48539  isubgr3stgrlem7  48621  grlimgrtri  48652  pgnbgreunbgrlem2  48766  pgnbgreunbgrlem5  48772