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

Theorem 3impdi 1348
Description: Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
Hypothesis
Ref Expression
3impdi.1 (((𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃)
Assertion
Ref Expression
3impdi ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impdi
StepHypRef Expression
1 3impdi.1 . . 3 (((𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃)
21anandis 677 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323impb 1113 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085
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 206  df-an 396  df-3an 1087
This theorem is referenced by:  oacan  8562  omcan  8583  ecovdi  8835  distrpi  10913  axltadd  11309  ccatlcan  14692  absmulgcd  16516  axlowdimlem14  28753  fh1  31415  fh2  31416  cm2j  31417  hoadddi  31600  hosubdi  31605  leopmul2i  31932  dvconstbi  43694  eel2131  44076  uun2131  44153  uun2131p1  44154  io1ii  47862  reccot  48112  rectan  48113
  Copyright terms: Public domain W3C validator