Theorem impcomd 415

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 414	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  sbequ2  2248  sbequ2OLD  2249  ralxfrd  5286  ralxfrd2  5290  iss  5888  funssres  6402  fv3  6713  fmptsnd  6962  frrlem10  8014  wfr3g  8031  nnmord  8338  cfcoflem  9851  nqereu  10508  ltletr  10889  fzind  12240  eqreznegel  12495  xrltletr  12712  xnn0xaddcl  12790  elfzodifsumelfzo  13273  hash2prde  14001  fundmge2nop0  14023  wrd2ind  14253  swrdccatin1  14255  rlimuni  15076  rlimno1  15182  ndvdssub  15933  lcmfunsnlem2  16160  coprmdvds  16173  coprmdvds2  16174  gsmsymgrfixlem1  18773  lsmdisj2  19026  chfacfisf  21705  chfacfisfcpmat  21706  lmcnp  22155  1stccnp  22313  txlm  22499  fgss2  22725  fgfil  22726  ufileu  22770  rnelfm  22804  fmfnfmlem2  22806  fmfnfmlem4  22808  ufilcmp  22883  cnpfcf  22892  alexsubALTlem2  22899  tsmsxp  23006  ivthlem2  24303  ivthlem3  24304  2sqreultlem  26282  2sqreultblem  26283  2sqreunnltlem  26285  2sqreunnltblem  26286  umgrislfupgrlem  27167  uhgr2edg  27250  wlkv0  27692  usgr2pth  27805  clwlkclwwlklem2  28037  frgrregord013  28432  prsrcmpltd  32722  sat1el2xp  33008  goalrlem  33025  dfpo2  33392