Theorem impcomd 416

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sbequ2  2285  ralxfrd  5381  ralxfrd2  5385  iss  6039  dfpo2  6299  funssres  6582  fv3  6901  fmptsnd  7169  resf1extb  7932  frrlem10  8293  wfr3g  8317  nnmord  8619  elirrv  9560  cfcoflem  10257  nqereu  10915  ltletr  11303  fzind  12695  eqreznegel  12959  xrltletr  13183  xnn0xaddcl  13262  elfzodifsumelfzo  13762  hash2prde  14509  hash3tpde  14532  fundmge2nop0  14541  wrd2ind  14762  swrdccatin1  14764  rlimuni  15603  rlimno1  15707  ndvdssub  16468  lcmfunsnlem2  16699  coprmdvds  16712  coprmdvds2  16713  gsmsymgrfixlem1  19498  lsmdisj2  19753  chfacfisf  22992  chfacfisfcpmat  22993  lmcnp  23442  1stccnp  23600  txlm  23786  fgss2  24012  fgfil  24013  ufileu  24057  rnelfm  24091  fmfnfmlem2  24093  fmfnfmlem4  24095  ufilcmp  24170  cnpfcf  24179  alexsubALTlem2  24186  tsmsxp  24293  ivthlem2  25592  ivthlem3  25593  2sqreultlem  27589  2sqreultblem  27590  2sqreunnltlem  27592  2sqreunnltblem  27593  negsid  28212  bdayons  28447  z12bdaylem  28655  umgrislfupgrlem  29450  uhgr2edg  29536  wlkv0  29977  usgr2pth  30091  clwlkclwwlklem2  30329  frgrregord013  30724  prsrcmpltd  35448  r1filimi  35475  sat1el2xp  35849  goalrlem  35866  axuntco  36968  uhgrimedgi  48632  isubgr3stgrlem7  48714  grlimgrtri  48745  pgnbgreunbgrlem2  48859  pgnbgreunbgrlem5  48865