Theorem impcomd 411

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sbequ2  2252  ralxfrd  5346  ralxfrd2  5350  iss  5984  dfpo2  6243  funssres  6525  fv3  6840  fmptsnd  7103  resf1extb  7864  frrlem10  8225  wfr3g  8249  nnmord  8547  cfcoflem  10160  nqereu  10817  ltletr  11202  fzind  12568  eqreznegel  12829  xrltletr  13053  xnn0xaddcl  13131  elfzodifsumelfzo  13628  hash2prde  14374  hash3tpde  14397  fundmge2nop0  14406  wrd2ind  14627  swrdccatin1  14629  rlimuni  15454  rlimno1  15558  ndvdssub  16317  lcmfunsnlem2  16548  coprmdvds  16561  coprmdvds2  16562  gsmsymgrfixlem1  19337  lsmdisj2  19592  chfacfisf  22767  chfacfisfcpmat  22768  lmcnp  23217  1stccnp  23375  txlm  23561  fgss2  23787  fgfil  23788  ufileu  23832  rnelfm  23866  fmfnfmlem2  23868  fmfnfmlem4  23870  ufilcmp  23945  cnpfcf  23954  alexsubALTlem2  23961  tsmsxp  24068  ivthlem2  25378  ivthlem3  25379  2sqreultlem  27383  2sqreultblem  27384  2sqreunnltlem  27386  2sqreunnltblem  27387  negsid  27981  bdayon  28207  umgrislfupgrlem  29098  uhgr2edg  29184  wlkv0  29626  usgr2pth  29740  clwlkclwwlklem2  29975  frgrregord013  30370  prsrcmpltd  35088  r1filimi  35106  sat1el2xp  35411  goalrlem  35428  uhgrimedgi  47920  isubgr3stgrlem7  48002  grlimgrtri  48033  pgnbgreunbgrlem2  48147  pgnbgreunbgrlem5  48153