MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impcomd Structured version   Visualization version   GIF version

Theorem impcomd 412
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
StepHypRef Expression
1 impd.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com23 86 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
32impd 411 1 (𝜑 → ((𝜒𝜓) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  sbequ2  2240  sbequ2OLD  2241  ralxfrd  5299  ralxfrd2  5303  iss  5896  funssres  6391  fv3  6681  fmptsnd  6923  wfr3g  7942  nnmord  8247  cfcoflem  9682  nqereu  10339  ltletr  10720  fzind  12068  eqreznegel  12322  xrltletr  12538  xnn0xaddcl  12616  elfzodifsumelfzo  13091  hash2prde  13816  fundmge2nop0  13838  wrd2ind  14073  swrdccatin1  14075  rlimuni  14895  rlimno1  14998  ndvdssub  15748  lcmfunsnlem2  15972  coprmdvds  15985  coprmdvds2  15986  gsmsymgrfixlem1  18484  lsmdisj2  18737  chfacfisf  21390  chfacfisfcpmat  21391  lmcnp  21840  1stccnp  21998  txlm  22184  fgss2  22410  fgfil  22411  ufileu  22455  rnelfm  22489  fmfnfmlem2  22491  fmfnfmlem4  22493  ufilcmp  22568  cnpfcf  22577  alexsubALTlem2  22584  tsmsxp  22690  ivthlem2  23980  ivthlem3  23981  2sqreultlem  25950  2sqreultblem  25951  2sqreunnltlem  25953  2sqreunnltblem  25954  umgrislfupgrlem  26834  uhgr2edg  26917  wlkv0  27359  usgr2pth  27472  clwlkclwwlklem2  27705  frgrregord013  28101  prsrcmpltd  32244  sat1el2xp  32523  goalrlem  32540  dfpo2  32888  frrlem10  33029
  Copyright terms: Public domain W3C validator