Theorem impcomd 414

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sbequ2  2250  sbequ2OLD  2251  ralxfrd  5309  ralxfrd2  5313  iss  5903  funssres  6398  fv3  6688  fmptsnd  6931  wfr3g  7953  nnmord  8258  cfcoflem  9694  nqereu  10351  ltletr  10732  fzind  12081  eqreznegel  12335  xrltletr  12551  xnn0xaddcl  12629  elfzodifsumelfzo  13104  hash2prde  13829  fundmge2nop0  13851  wrd2ind  14085  swrdccatin1  14087  rlimuni  14907  rlimno1  15010  ndvdssub  15760  lcmfunsnlem2  15984  coprmdvds  15997  coprmdvds2  15998  gsmsymgrfixlem1  18555  lsmdisj2  18808  chfacfisf  21462  chfacfisfcpmat  21463  lmcnp  21912  1stccnp  22070  txlm  22256  fgss2  22482  fgfil  22483  ufileu  22527  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  ufilcmp  22640  cnpfcf  22649  alexsubALTlem2  22656  tsmsxp  22763  ivthlem2  24053  ivthlem3  24054  2sqreultlem  26023  2sqreultblem  26024  2sqreunnltlem  26026  2sqreunnltblem  26027  umgrislfupgrlem  26907  uhgr2edg  26990  wlkv0  27432  usgr2pth  27545  clwlkclwwlklem2  27778  frgrregord013  28174  prsrcmpltd  32347  sat1el2xp  32626  goalrlem  32643  dfpo2  32991  frrlem10  33132