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  2250  ralxfrd  5350  ralxfrd2  5354  iss  5990  dfpo2  6248  funssres  6530  fv3  6844  fmptsnd  7109  resf1extb  7874  frrlem10  8235  wfr3g  8259  nnmord  8557  cfcoflem  10185  nqereu  10842  ltletr  11226  fzind  12592  eqreznegel  12853  xrltletr  13077  xnn0xaddcl  13155  elfzodifsumelfzo  13652  hash2prde  14395  hash3tpde  14418  fundmge2nop0  14427  wrd2ind  14647  swrdccatin1  14649  rlimuni  15475  rlimno1  15579  ndvdssub  16338  lcmfunsnlem2  16569  coprmdvds  16582  coprmdvds2  16583  gsmsymgrfixlem1  19324  lsmdisj2  19579  chfacfisf  22757  chfacfisfcpmat  22758  lmcnp  23207  1stccnp  23365  txlm  23551  fgss2  23777  fgfil  23778  ufileu  23822  rnelfm  23856  fmfnfmlem2  23858  fmfnfmlem4  23860  ufilcmp  23935  cnpfcf  23944  alexsubALTlem2  23951  tsmsxp  24058  ivthlem2  25369  ivthlem3  25370  2sqreultlem  27374  2sqreultblem  27375  2sqreunnltlem  27377  2sqreunnltblem  27378  negsid  27970  bdayon  28196  umgrislfupgrlem  29085  uhgr2edg  29171  wlkv0  29613  usgr2pth  29727  clwlkclwwlklem2  29962  frgrregord013  30357  prsrcmpltd  35047  sat1el2xp  35351  goalrlem  35368  uhgrimedgi  47875  isubgr3stgrlem7  47957  grlimgrtri  47988  pgnbgreunbgrlem2  48102  pgnbgreunbgrlem5  48108