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

Theorem 3impdi 1351
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 678 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323impb 1115 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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  df-3an 1089
This theorem is referenced by:  oacan  8586  omcan  8607  ecovdi  8865  distrpi  10938  axltadd  11334  ccatlcan  14756  absmulgcd  16586  axlowdimlem14  28970  fh1  31637  fh2  31638  cm2j  31639  hoadddi  31822  hosubdi  31827  leopmul2i  32154  dvconstbi  44353  eel2131  44734  uun2131  44811  uun2131p1  44812  io1ii  48818  reccot  49277  rectan  49278
  Copyright terms: Public domain W3C validator