Theorem impcomd 412

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sbequ2  2261  ralxfrd  5344  ralxfrd2  5348  iss  5994  dfpo2  6254  funssres  6536  fv3  6852  fmptsnd  7120  resf1extb  7881  frrlem10  8242  wfr3g  8266  nnmord  8565  elirrv  9509  cfcoflem  10192  nqereu  10850  ltletr  11236  fzind  12625  eqreznegel  12882  xrltletr  13106  xnn0xaddcl  13185  elfzodifsumelfzo  13684  hash2prde  14430  hash3tpde  14453  fundmge2nop0  14462  wrd2ind  14683  swrdccatin1  14685  rlimuni  15510  rlimno1  15614  ndvdssub  16376  lcmfunsnlem2  16607  coprmdvds  16620  coprmdvds2  16621  gsmsymgrfixlem1  19400  lsmdisj2  19655  chfacfisf  22844  chfacfisfcpmat  22845  lmcnp  23294  1stccnp  23452  txlm  23638  fgss2  23864  fgfil  23865  ufileu  23909  rnelfm  23943  fmfnfmlem2  23945  fmfnfmlem4  23947  ufilcmp  24022  cnpfcf  24031  alexsubALTlem2  24038  tsmsxp  24145  ivthlem2  25444  ivthlem3  25445  2sqreultlem  27435  2sqreultblem  27436  2sqreunnltlem  27438  2sqreunnltblem  27439  negsid  28058  bdayons  28293  z12bdaylem  28501  umgrislfupgrlem  29216  uhgr2edg  29302  wlkv0  29743  usgr2pth  29857  clwlkclwwlklem2  30095  frgrregord013  30490  prsrcmpltd  35270  r1filimi  35291  sat1el2xp  35614  goalrlem  35631  axuntco  36714  uhgrimedgi  48388  isubgr3stgrlem7  48470  grlimgrtri  48501  pgnbgreunbgrlem2  48615  pgnbgreunbgrlem5  48621