Theorem impcomd 417

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sbequ2  2288  prsrcmpltd  4443  ralxfrd  5384  ralxfrd2  5388  iss  6042  dfpo2  6304  funssres  6587  fv3  6906  fmptsnd  7174  resf1extb  7940  frrlem10  8301  wfr3g  8325  nnmord  8627  elirrv  9569  cfcoflem  10274  nqereu  10932  ltletr  11320  fzind  12712  eqreznegel  12976  xrltletr  13200  xnn0xaddcl  13279  elfzodifsumelfzo  13779  hash2prde  14527  hash3tpde  14550  fundmge2nop0  14559  wrd2ind  14784  swrdccatin1  14786  rlimuni  15627  rlimno1  15731  ndvdssub  16492  lcmfunsnlem2  16723  coprmdvds  16736  coprmdvds2  16737  gsmsymgrfixlem1  19528  lsmdisj2  19783  chfacfisf  23048  chfacfisfcpmat  23049  lmcnp  23498  1stccnp  23656  txlm  23842  fgss2  24068  fgfil  24069  ufileu  24113  rnelfm  24147  fmfnfmlem2  24149  fmfnfmlem4  24151  ufilcmp  24226  cnpfcf  24235  alexsubALTlem2  24242  tsmsxp  24349  ivthlem2  25648  ivthlem3  25649  2sqreultlem  27648  2sqreultblem  27649  2sqreunnltlem  27651  2sqreunnltblem  27652  negsid  28271  bdayons  28506  z12bdaylem  28714  umgrislfupgrlem  29509  uhgr2edg  29595  wlkv0  30036  usgr2pth  30150  clwlkclwwlklem2  30388  frgrregord013  30783  r1filimi  35522  sat1el2xp  35892  goalrlem  35909  axuntco  37031  uhgrimedgi  48696  isubgr3stgrlem7  48778  grlimgrtri  48809  pgnbgreunbgrlem2  48923  pgnbgreunbgrlem5  48929