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  5345  ralxfrd2  5349  iss  5994  dfpo2  6254  funssres  6536  fv3  6852  fmptsnd  7117  resf1extb  7878  frrlem10  8238  wfr3g  8262  nnmord  8561  cfcoflem  10185  nqereu  10843  ltletr  11229  fzind  12618  eqreznegel  12875  xrltletr  13099  xnn0xaddcl  13178  elfzodifsumelfzo  13677  hash2prde  14423  hash3tpde  14446  fundmge2nop0  14455  wrd2ind  14676  swrdccatin1  14678  rlimuni  15503  rlimno1  15607  ndvdssub  16369  lcmfunsnlem2  16600  coprmdvds  16613  coprmdvds2  16614  gsmsymgrfixlem1  19393  lsmdisj2  19648  chfacfisf  22829  chfacfisfcpmat  22830  lmcnp  23279  1stccnp  23437  txlm  23623  fgss2  23849  fgfil  23850  ufileu  23894  rnelfm  23928  fmfnfmlem2  23930  fmfnfmlem4  23932  ufilcmp  24007  cnpfcf  24016  alexsubALTlem2  24023  tsmsxp  24130  ivthlem2  25429  ivthlem3  25430  2sqreultlem  27424  2sqreultblem  27425  2sqreunnltlem  27427  2sqreunnltblem  27428  negsid  28047  bdayons  28282  z12bdaylem  28490  umgrislfupgrlem  29205  uhgr2edg  29291  wlkv0  29733  usgr2pth  29847  clwlkclwwlklem2  30085  frgrregord013  30480  prsrcmpltd  35239  r1filimi  35262  sat1el2xp  35577  goalrlem  35594  axuntco  36677  uhgrimedgi  48378  isubgr3stgrlem7  48460  grlimgrtri  48491  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem5  48611