Theorem impcomd 415

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sbequ2  2283  ralxfrd  5364  ralxfrd2  5368  iss  6021  dfpo2  6279  funssres  6561  fv3  6881  fmptsnd  7149  resf1extb  7911  frrlem10  8271  wfr3g  8295  nnmord  8597  elirrv  9542  cfcoflem  10226  nqereu  10884  ltletr  11272  fzind  12668  eqreznegel  12932  xrltletr  13156  xnn0xaddcl  13235  elfzodifsumelfzo  13734  hash2prde  14480  hash3tpde  14503  fundmge2nop0  14512  wrd2ind  14733  swrdccatin1  14735  rlimuni  15560  rlimno1  15664  ndvdssub  16426  lcmfunsnlem2  16657  coprmdvds  16670  coprmdvds2  16671  gsmsymgrfixlem1  19450  lsmdisj2  19705  chfacfisf  22894  chfacfisfcpmat  22895  lmcnp  23344  1stccnp  23502  txlm  23688  fgss2  23914  fgfil  23915  ufileu  23959  rnelfm  23993  fmfnfmlem2  23995  fmfnfmlem4  23997  ufilcmp  24072  cnpfcf  24081  alexsubALTlem2  24088  tsmsxp  24195  ivthlem2  25494  ivthlem3  25495  2sqreultlem  27488  2sqreultblem  27489  2sqreunnltlem  27491  2sqreunnltblem  27492  negsid  28111  bdayons  28346  z12bdaylem  28554  umgrislfupgrlem  29269  uhgr2edg  29355  wlkv0  29796  usgr2pth  29910  clwlkclwwlklem2  30148  frgrregord013  30543  prsrcmpltd  35340  r1filimi  35363  sat1el2xp  35693  goalrlem  35710  axuntco  36803  uhgrimedgi  48476  isubgr3stgrlem7  48558  grlimgrtri  48589  pgnbgreunbgrlem2  48703  pgnbgreunbgrlem5  48709