Theorem impcomd 417

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 416	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sbequ2  2284  prsrcmpltd  4432  ralxfrd  5369  ralxfrd2  5373  iss  6026  dfpo2  6299  funssres  6584  fv3  6903  fmptsnd  7174  resf1extb  7946  frrlem10  8316  wfr3g  8340  nnmord  8644  elirrv  9594  r1filimi  9906  cfcoflem  10353  nqereu  11017  ltletr  11405  fzind  12800  eqreznegel  13064  xrltletr  13289  xnn0xaddcl  13368  elfzodifsumelfzo  13869  hash2prde  14618  hash3tpde  14641  fundmge2nop0  14650  wrd2ind  14876  swrdccatin1  14878  rlimuni  15722  rlimno1  15826  ndvdssub  16584  lcmfunsnlem2  16820  coprmdvds  16833  coprmdvds2  16834  mgmn0plusgplusf  18833  gsmsymgrfixlem1  19646  lsmdisj2  19901  chfacfisf  23177  chfacfisfcpmat  23178  lmcnp  23627  1stccnp  23786  txlm  23972  fgss2  24198  fgfil  24199  ufileu  24243  rnelfm  24277  fmfnfmlem2  24279  fmfnfmlem4  24281  ufilcmp  24356  cnpfcf  24365  alexsubALTlem2  24372  tsmsxp  24479  ivthlem2  25778  ivthlem3  25779  2sqreultlem  27779  2sqreultblem  27780  2sqreunnltlem  27782  2sqreunnltblem  27783  fltoprm  28000  negsid  28432  bdayons  28667  z12bdaylem  28875  umgrislfupgrlem  29705  uhgr2edg  29794  wlkv0  30235  usgr2pth  30355  clwlkclwwlklem2  30596  frgrregord013  31001  sat1el2xp  36230  goalrlem  36247  axuntco  37359  uhgrimedgi  49081  isubgr3stgrlem7  49163  grlimgrtri  49194  pgnbgreunbgrlem2  49308  pgnbgreunbgrlem5  49314