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

Theorem 3impdi 1372
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 868 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323impb 1251 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  oacan  7492  omcan  7513  ecovdi  7720  distrpi  9576  axltadd  9962  ccatlcan  13270  absmulgcd  15050  axlowdimlem14  25553  fh1  27667  fh2  27668  cm2j  27669  hoadddi  27852  hosubdi  27857  leopmul2i  28184  dvconstbi  37351  eel2131  37756  uun2131  37835  uun2131p1  37836  reccot  42254  rectan  42255
  Copyright terms: Public domain W3C validator