Theorem impcomd 412

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  sbequ2  2241  ralxfrd  5368  ralxfrd2  5372  iss  5994  dfpo2  6253  funssres  6550  fv3  6865  fmptsnd  7120  frrlem10  8231  wfr3g  8258  nnmord  8584  cfcoflem  10217  nqereu  10874  ltletr  11256  fzind  12610  eqreznegel  12868  xrltletr  13086  xnn0xaddcl  13164  elfzodifsumelfzo  13648  hash2prde  14381  fundmge2nop0  14403  wrd2ind  14623  swrdccatin1  14625  rlimuni  15444  rlimno1  15550  ndvdssub  16302  lcmfunsnlem2  16527  coprmdvds  16540  coprmdvds2  16541  gsmsymgrfixlem1  19223  lsmdisj2  19478  chfacfisf  22240  chfacfisfcpmat  22241  lmcnp  22692  1stccnp  22850  txlm  23036  fgss2  23262  fgfil  23263  ufileu  23307  rnelfm  23341  fmfnfmlem2  23343  fmfnfmlem4  23345  ufilcmp  23420  cnpfcf  23429  alexsubALTlem2  23436  tsmsxp  23543  ivthlem2  24853  ivthlem3  24854  2sqreultlem  26832  2sqreultblem  26833  2sqreunnltlem  26835  2sqreunnltblem  26836  negsid  27382  umgrislfupgrlem  28136  uhgr2edg  28219  wlkv0  28662  usgr2pth  28775  clwlkclwwlklem2  29007  frgrregord013  29402  prsrcmpltd  33776  sat1el2xp  34060  goalrlem  34077