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  5406  ralxfrd2  5410  iss  6035  dfpo2  6295  funssres  6592  fv3  6909  fmptsnd  7169  frrlem10  8282  wfr3g  8309  nnmord  8634  cfcoflem  10269  nqereu  10926  ltletr  11310  fzind  12664  eqreznegel  12922  xrltletr  13140  xnn0xaddcl  13218  elfzodifsumelfzo  13702  hash2prde  14435  fundmge2nop0  14457  wrd2ind  14677  swrdccatin1  14679  rlimuni  15498  rlimno1  15604  ndvdssub  16356  lcmfunsnlem2  16581  coprmdvds  16594  coprmdvds2  16595  gsmsymgrfixlem1  19336  lsmdisj2  19591  chfacfisf  22576  chfacfisfcpmat  22577  lmcnp  23028  1stccnp  23186  txlm  23372  fgss2  23598  fgfil  23599  ufileu  23643  rnelfm  23677  fmfnfmlem2  23679  fmfnfmlem4  23681  ufilcmp  23756  cnpfcf  23765  alexsubALTlem2  23772  tsmsxp  23879  ivthlem2  25193  ivthlem3  25194  2sqreultlem  27174  2sqreultblem  27175  2sqreunnltlem  27177  2sqreunnltblem  27178  negsid  27742  umgrislfupgrlem  28637  uhgr2edg  28720  wlkv0  29163  usgr2pth  29276  clwlkclwwlklem2  29508  frgrregord013  29903  prsrcmpltd  34372  sat1el2xp  34656  goalrlem  34673