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

Theorem impcomd 415
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 414 1 (𝜑 → ((𝜒𝜓) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  sbequ2  2249  sbequ2OLD  2250  ralxfrd  5277  ralxfrd2  5281  iss  5874  funssres  6372  fv3  6667  fmptsnd  6912  wfr3g  7940  nnmord  8245  cfcoflem  9687  nqereu  10344  ltletr  10725  fzind  12072  eqreznegel  12326  xrltletr  12542  xnn0xaddcl  12620  elfzodifsumelfzo  13102  hash2prde  13828  fundmge2nop0  13850  wrd2ind  14080  swrdccatin1  14082  rlimuni  14903  rlimno1  15006  ndvdssub  15754  lcmfunsnlem2  15978  coprmdvds  15991  coprmdvds2  15992  gsmsymgrfixlem1  18551  lsmdisj2  18804  chfacfisf  21463  chfacfisfcpmat  21464  lmcnp  21913  1stccnp  22071  txlm  22257  fgss2  22483  fgfil  22484  ufileu  22528  rnelfm  22562  fmfnfmlem2  22564  fmfnfmlem4  22566  ufilcmp  22641  cnpfcf  22650  alexsubALTlem2  22657  tsmsxp  22764  ivthlem2  24060  ivthlem3  24061  2sqreultlem  26035  2sqreultblem  26036  2sqreunnltlem  26038  2sqreunnltblem  26039  umgrislfupgrlem  26919  uhgr2edg  27002  wlkv0  27444  usgr2pth  27557  clwlkclwwlklem2  27789  frgrregord013  28184  prsrcmpltd  32461  sat1el2xp  32740  goalrlem  32757  dfpo2  33105  frrlem10  33246
  Copyright terms: Public domain W3C validator