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  2257  ralxfrd  5350  ralxfrd2  5354  iss  6000  dfpo2  6260  funssres  6542  fv3  6858  fmptsnd  7124  resf1extb  7885  frrlem10  8245  wfr3g  8269  nnmord  8568  cfcoflem  10194  nqereu  10852  ltletr  11238  fzind  12627  eqreznegel  12884  xrltletr  13108  xnn0xaddcl  13187  elfzodifsumelfzo  13686  hash2prde  14432  hash3tpde  14455  fundmge2nop0  14464  wrd2ind  14685  swrdccatin1  14687  rlimuni  15512  rlimno1  15616  ndvdssub  16378  lcmfunsnlem2  16609  coprmdvds  16622  coprmdvds2  16623  gsmsymgrfixlem1  19402  lsmdisj2  19657  chfacfisf  22819  chfacfisfcpmat  22820  lmcnp  23269  1stccnp  23427  txlm  23613  fgss2  23839  fgfil  23840  ufileu  23884  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  ufilcmp  23997  cnpfcf  24006  alexsubALTlem2  24013  tsmsxp  24120  ivthlem2  25419  ivthlem3  25420  2sqreultlem  27410  2sqreultblem  27411  2sqreunnltlem  27413  2sqreunnltblem  27414  negsid  28033  bdayons  28268  z12bdaylem  28476  umgrislfupgrlem  29191  uhgr2edg  29277  wlkv0  29718  usgr2pth  29832  clwlkclwwlklem2  30070  frgrregord013  30465  prsrcmpltd  35223  r1filimi  35246  sat1el2xp  35561  goalrlem  35578  axuntco  36661  uhgrimedgi  48366  isubgr3stgrlem7  48448  grlimgrtri  48479  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem5  48599