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  2256  ralxfrd  5353  ralxfrd2  5357  iss  5994  dfpo2  6254  funssres  6536  fv3  6852  fmptsnd  7115  resf1extb  7876  frrlem10  8237  wfr3g  8261  nnmord  8560  cfcoflem  10182  nqereu  10840  ltletr  11225  fzind  12590  eqreznegel  12847  xrltletr  13071  xnn0xaddcl  13150  elfzodifsumelfzo  13647  hash2prde  14393  hash3tpde  14416  fundmge2nop0  14425  wrd2ind  14646  swrdccatin1  14648  rlimuni  15473  rlimno1  15577  ndvdssub  16336  lcmfunsnlem2  16567  coprmdvds  16580  coprmdvds2  16581  gsmsymgrfixlem1  19356  lsmdisj2  19611  chfacfisf  22798  chfacfisfcpmat  22799  lmcnp  23248  1stccnp  23406  txlm  23592  fgss2  23818  fgfil  23819  ufileu  23863  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem4  23901  ufilcmp  23976  cnpfcf  23985  alexsubALTlem2  23992  tsmsxp  24099  ivthlem2  25409  ivthlem3  25410  2sqreultlem  27414  2sqreultblem  27415  2sqreunnltlem  27417  2sqreunnltblem  27418  negsid  28037  bdayons  28272  z12bdaylem  28480  umgrislfupgrlem  29195  uhgr2edg  29281  wlkv0  29723  usgr2pth  29837  clwlkclwwlklem2  30075  frgrregord013  30470  prsrcmpltd  35237  r1filimi  35259  sat1el2xp  35573  goalrlem  35590  uhgrimedgi  48132  isubgr3stgrlem7  48214  grlimgrtri  48245  pgnbgreunbgrlem2  48359  pgnbgreunbgrlem5  48365