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  2249  ralxfrd  5408  ralxfrd2  5412  iss  6053  dfpo2  6316  funssres  6610  fv3  6924  fmptsnd  7189  resf1extb  7956  frrlem10  8320  wfr3g  8347  nnmord  8670  cfcoflem  10312  nqereu  10969  ltletr  11353  fzind  12716  eqreznegel  12976  xrltletr  13199  xnn0xaddcl  13277  elfzodifsumelfzo  13770  hash2prde  14509  hash3tpde  14532  fundmge2nop0  14541  wrd2ind  14761  swrdccatin1  14763  rlimuni  15586  rlimno1  15690  ndvdssub  16446  lcmfunsnlem2  16677  coprmdvds  16690  coprmdvds2  16691  gsmsymgrfixlem1  19445  lsmdisj2  19700  chfacfisf  22860  chfacfisfcpmat  22861  lmcnp  23312  1stccnp  23470  txlm  23656  fgss2  23882  fgfil  23883  ufileu  23927  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem4  23965  ufilcmp  24040  cnpfcf  24049  alexsubALTlem2  24056  tsmsxp  24163  ivthlem2  25487  ivthlem3  25488  2sqreultlem  27491  2sqreultblem  27492  2sqreunnltlem  27494  2sqreunnltblem  27495  negsid  28073  umgrislfupgrlem  29139  uhgr2edg  29225  wlkv0  29669  usgr2pth  29784  clwlkclwwlklem2  30019  frgrregord013  30414  prsrcmpltd  35095  sat1el2xp  35384  goalrlem  35401  isubgr3stgrlem7  47939  grlimgrtri  47963