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  2285  prsrcmpltd  4433  ralxfrd  5370  ralxfrd2  5374  iss  6029  dfpo2  6292  funssres  6576  fv3  6895  fmptsnd  7166  resf1extb  7935  frrlem10  8297  wfr3g  8321  nnmord  8625  elirrv  9575  r1filimi  9884  cfcoflem  10331  nqereu  10995  ltletr  11383  fzind  12778  eqreznegel  13042  xrltletr  13267  xnn0xaddcl  13346  elfzodifsumelfzo  13846  hash2prde  14595  hash3tpde  14618  fundmge2nop0  14627  wrd2ind  14852  swrdccatin1  14854  rlimuni  15697  rlimno1  15801  ndvdssub  16559  lcmfunsnlem2  16795  coprmdvds  16808  coprmdvds2  16809  mgmn0plusgplusf  18808  gsmsymgrfixlem1  19621  lsmdisj2  19876  chfacfisf  23152  chfacfisfcpmat  23153  lmcnp  23602  1stccnp  23761  txlm  23947  fgss2  24173  fgfil  24174  ufileu  24218  rnelfm  24252  fmfnfmlem2  24254  fmfnfmlem4  24256  ufilcmp  24331  cnpfcf  24340  alexsubALTlem2  24347  tsmsxp  24454  ivthlem2  25753  ivthlem3  25754  2sqreultlem  27756  2sqreultblem  27757  2sqreunnltlem  27759  2sqreunnltblem  27760  fltoprm  27977  negsid  28409  bdayons  28644  z12bdaylem  28852  umgrislfupgrlem  29682  uhgr2edg  29771  wlkv0  30212  usgr2pth  30332  clwlkclwwlklem2  30573  frgrregord013  30978  sat1el2xp  36113  goalrlem  36130  axuntco  37237  uhgrimedgi  48932  isubgr3stgrlem7  49014  grlimgrtri  49045  pgnbgreunbgrlem2  49159  pgnbgreunbgrlem5  49165