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  5426  ralxfrd2  5430  iss  6064  dfpo2  6327  funssres  6622  fv3  6938  fmptsnd  7203  frrlem10  8336  wfr3g  8363  nnmord  8688  cfcoflem  10341  nqereu  10998  ltletr  11382  fzind  12741  eqreznegel  12999  xrltletr  13219  xnn0xaddcl  13297  elfzodifsumelfzo  13782  hash2prde  14519  hash3tpde  14542  fundmge2nop0  14551  wrd2ind  14771  swrdccatin1  14773  rlimuni  15596  rlimno1  15702  ndvdssub  16457  lcmfunsnlem2  16687  coprmdvds  16700  coprmdvds2  16701  gsmsymgrfixlem1  19469  lsmdisj2  19724  chfacfisf  22881  chfacfisfcpmat  22882  lmcnp  23333  1stccnp  23491  txlm  23677  fgss2  23903  fgfil  23904  ufileu  23948  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem4  23986  ufilcmp  24061  cnpfcf  24070  alexsubALTlem2  24077  tsmsxp  24184  ivthlem2  25506  ivthlem3  25507  2sqreultlem  27509  2sqreultblem  27510  2sqreunnltlem  27512  2sqreunnltblem  27513  negsid  28091  umgrislfupgrlem  29157  uhgr2edg  29243  wlkv0  29687  usgr2pth  29800  clwlkclwwlklem2  30032  frgrregord013  30427  prsrcmpltd  35057  sat1el2xp  35347  goalrlem  35364  grlimgrtri  47820