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  5378  ralxfrd2  5382  iss  6022  dfpo2  6285  funssres  6580  fv3  6894  fmptsnd  7161  resf1extb  7930  frrlem10  8294  wfr3g  8321  nnmord  8644  cfcoflem  10286  nqereu  10943  ltletr  11327  fzind  12691  eqreznegel  12950  xrltletr  13173  xnn0xaddcl  13251  elfzodifsumelfzo  13747  hash2prde  14488  hash3tpde  14511  fundmge2nop0  14520  wrd2ind  14741  swrdccatin1  14743  rlimuni  15566  rlimno1  15670  ndvdssub  16428  lcmfunsnlem2  16659  coprmdvds  16672  coprmdvds2  16673  gsmsymgrfixlem1  19408  lsmdisj2  19663  chfacfisf  22792  chfacfisfcpmat  22793  lmcnp  23242  1stccnp  23400  txlm  23586  fgss2  23812  fgfil  23813  ufileu  23857  rnelfm  23891  fmfnfmlem2  23893  fmfnfmlem4  23895  ufilcmp  23970  cnpfcf  23979  alexsubALTlem2  23986  tsmsxp  24093  ivthlem2  25405  ivthlem3  25406  2sqreultlem  27410  2sqreultblem  27411  2sqreunnltlem  27413  2sqreunnltblem  27414  negsid  27999  bdayon  28225  umgrislfupgrlem  29101  uhgr2edg  29187  wlkv0  29631  usgr2pth  29746  clwlkclwwlklem2  29981  frgrregord013  30376  prsrcmpltd  35112  sat1el2xp  35401  goalrlem  35418  uhgrimedgi  47903  isubgr3stgrlem7  47984  grlimgrtri  48008