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  2252  ralxfrd  5344  ralxfrd2  5348  iss  5983  dfpo2  6243  funssres  6525  fv3  6840  fmptsnd  7103  resf1extb  7864  frrlem10  8225  wfr3g  8249  nnmord  8547  cfcoflem  10163  nqereu  10820  ltletr  11205  fzind  12571  eqreznegel  12832  xrltletr  13056  xnn0xaddcl  13134  elfzodifsumelfzo  13631  hash2prde  14377  hash3tpde  14400  fundmge2nop0  14409  wrd2ind  14630  swrdccatin1  14632  rlimuni  15457  rlimno1  15561  ndvdssub  16320  lcmfunsnlem2  16551  coprmdvds  16564  coprmdvds2  16565  gsmsymgrfixlem1  19339  lsmdisj2  19594  chfacfisf  22769  chfacfisfcpmat  22770  lmcnp  23219  1stccnp  23377  txlm  23563  fgss2  23789  fgfil  23790  ufileu  23834  rnelfm  23868  fmfnfmlem2  23870  fmfnfmlem4  23872  ufilcmp  23947  cnpfcf  23956  alexsubALTlem2  23963  tsmsxp  24070  ivthlem2  25380  ivthlem3  25381  2sqreultlem  27385  2sqreultblem  27386  2sqreunnltlem  27388  2sqreunnltblem  27389  negsid  27983  bdayon  28209  umgrislfupgrlem  29100  uhgr2edg  29186  wlkv0  29628  usgr2pth  29742  clwlkclwwlklem2  29980  frgrregord013  30375  prsrcmpltd  35093  r1filimi  35114  sat1el2xp  35423  goalrlem  35440  uhgrimedgi  47989  isubgr3stgrlem7  48071  grlimgrtri  48102  pgnbgreunbgrlem2  48216  pgnbgreunbgrlem5  48222