Theorem impcomd 413

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  sbequ2  2242  ralxfrd  5407  ralxfrd2  5411  iss  6036  dfpo2  6296  funssres  6593  fv3  6910  fmptsnd  7167  frrlem10  8280  wfr3g  8307  nnmord  8632  cfcoflem  10267  nqereu  10924  ltletr  11306  fzind  12660  eqreznegel  12918  xrltletr  13136  xnn0xaddcl  13214  elfzodifsumelfzo  13698  hash2prde  14431  fundmge2nop0  14453  wrd2ind  14673  swrdccatin1  14675  rlimuni  15494  rlimno1  15600  ndvdssub  16352  lcmfunsnlem2  16577  coprmdvds  16590  coprmdvds2  16591  gsmsymgrfixlem1  19295  lsmdisj2  19550  chfacfisf  22356  chfacfisfcpmat  22357  lmcnp  22808  1stccnp  22966  txlm  23152  fgss2  23378  fgfil  23379  ufileu  23423  rnelfm  23457  fmfnfmlem2  23459  fmfnfmlem4  23461  ufilcmp  23536  cnpfcf  23545  alexsubALTlem2  23552  tsmsxp  23659  ivthlem2  24969  ivthlem3  24970  2sqreultlem  26950  2sqreultblem  26951  2sqreunnltlem  26953  2sqreunnltblem  26954  negsid  27515  umgrislfupgrlem  28382  uhgr2edg  28465  wlkv0  28908  usgr2pth  29021  clwlkclwwlklem2  29253  frgrregord013  29648  prsrcmpltd  34086  sat1el2xp  34370  goalrlem  34387