Theorem impcomd 416

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 87	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	impd 415	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sbequ2  2287  ralxfrd  5370  ralxfrd2  5374  iss  6028  dfpo2  6287  funssres  6569  fv3  6889  fmptsnd  7157  resf1extb  7919  frrlem10  8280  wfr3g  8304  nnmord  8606  elirrv  9547  cfcoflem  10244  nqereu  10902  ltletr  11290  fzind  12685  eqreznegel  12949  xrltletr  13173  xnn0xaddcl  13252  elfzodifsumelfzo  13751  hash2prde  14497  hash3tpde  14520  fundmge2nop0  14529  wrd2ind  14750  swrdccatin1  14752  rlimuni  15591  rlimno1  15695  ndvdssub  16457  lcmfunsnlem2  16688  coprmdvds  16701  coprmdvds2  16702  gsmsymgrfixlem1  19488  lsmdisj2  19743  chfacfisf  22972  chfacfisfcpmat  22973  lmcnp  23422  1stccnp  23580  txlm  23766  fgss2  23992  fgfil  23993  ufileu  24037  rnelfm  24071  fmfnfmlem2  24073  fmfnfmlem4  24075  ufilcmp  24150  cnpfcf  24159  alexsubALTlem2  24166  tsmsxp  24273  ivthlem2  25572  ivthlem3  25573  2sqreultlem  27569  2sqreultblem  27570  2sqreunnltlem  27572  2sqreunnltblem  27573  negsid  28192  bdayons  28427  z12bdaylem  28635  umgrislfupgrlem  29381  uhgr2edg  29467  wlkv0  29908  usgr2pth  30022  clwlkclwwlklem2  30260  frgrregord013  30655  prsrcmpltd  35386  r1filimi  35411  sat1el2xp  35742  goalrlem  35759  axuntco  36852  uhgrimedgi  48510  isubgr3stgrlem7  48592  grlimgrtri  48623  pgnbgreunbgrlem2  48737  pgnbgreunbgrlem5  48743