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  2286  prsrcmpltd  4436  ralxfrd  5377  ralxfrd2  5381  iss  6035  dfpo2  6298  funssres  6581  fv3  6900  fmptsnd  7171  resf1extb  7935  frrlem10  8298  wfr3g  8322  nnmord  8624  elirrv  9573  cfcoflem  10278  nqereu  10942  ltletr  11330  fzind  12723  eqreznegel  12987  xrltletr  13212  xnn0xaddcl  13291  elfzodifsumelfzo  13791  hash2prde  14539  hash3tpde  14562  fundmge2nop0  14571  wrd2ind  14796  swrdccatin1  14798  rlimuni  15641  rlimno1  15745  ndvdssub  16505  lcmfunsnlem2  16736  coprmdvds  16749  coprmdvds2  16750  mgmn0plusgplusf  18748  gsmsymgrfixlem1  19560  lsmdisj2  19815  chfacfisf  23085  chfacfisfcpmat  23086  lmcnp  23535  1stccnp  23694  txlm  23880  fgss2  24106  fgfil  24107  ufileu  24151  rnelfm  24185  fmfnfmlem2  24187  fmfnfmlem4  24189  ufilcmp  24264  cnpfcf  24273  alexsubALTlem2  24280  tsmsxp  24387  ivthlem2  25686  ivthlem3  25687  2sqreultlem  27691  2sqreultblem  27692  2sqreunnltlem  27694  2sqreunnltblem  27695  negsid  28314  bdayons  28549  z12bdaylem  28757  umgrislfupgrlem  29587  uhgr2edg  29676  wlkv0  30117  usgr2pth  30237  clwlkclwwlklem2  30478  frgrregord013  30883  r1filimi  35619  sat1el2xp  35966  goalrlem  35983  axuntco  37106  uhgrimedgi  48814  isubgr3stgrlem7  48896  grlimgrtri  48927  pgnbgreunbgrlem2  49041  pgnbgreunbgrlem5  49047