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  4436  ralxfrd  5374  ralxfrd2  5378  iss  6039  dfpo2  6317  funssres  6604  fv3  6926  fmptsnd  7197  resf1extb  7970  frrlem10  8341  wfr3g  8365  nnmord  8669  elirrv  9618  r1filimi  9930  cfcoflem  10377  nqereu  11041  ltletr  11429  fzind  12824  eqreznegel  13088  xrltletr  13313  xnn0xaddcl  13392  elfzodifsumelfzo  13893  hash2prde  14642  hash3tpde  14665  fundmge2nop0  14674  wrd2ind  14900  swrdccatin1  14902  rlimuni  15746  rlimno1  15850  ndvdssub  16608  lcmfunsnlem2  16844  coprmdvds  16857  coprmdvds2  16858  mgmn0plusgplusf  18857  gsmsymgrfixlem1  19671  lsmdisj2  19926  chfacfisf  23202  chfacfisfcpmat  23203  lmcnp  23652  1stccnp  23811  txlm  23997  fgss2  24223  fgfil  24224  ufileu  24268  rnelfm  24302  fmfnfmlem2  24304  fmfnfmlem4  24306  ufilcmp  24381  cnpfcf  24390  alexsubALTlem2  24397  tsmsxp  24504  ivthlem2  25803  ivthlem3  25804  2sqreultlem  27804  2sqreultblem  27805  2sqreunnltlem  27807  2sqreunnltblem  27808  fltoprm  28025  negsid  28457  bdayons  28692  z12bdaylem  28900  umgrislfupgrlem  29730  uhgr2edg  29819  wlkv0  30260  usgr2pth  30380  clwlkclwwlklem2  30621  frgrregord013  31026  sat1el2xp  36311  goalrlem  36328  elpssmo  36636  axuntco  37445  uhgrimedgi  49193  isubgr3stgrlem7  49275  grlimgrtri  49306  pgnbgreunbgrlem2  49420  pgnbgreunbgrlem5  49426