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

Theorem 3impdi 1343
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 674 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323impb 1108 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080
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  df-3an 1082
This theorem is referenced by:  oacan  8031  omcan  8052  ecovdi  8262  distrpi  10173  axltadd  10567  ccatlcan  13920  absmulgcd  15730  axlowdimlem14  26428  fh1  29082  fh2  29083  cm2j  29084  hoadddi  29267  hosubdi  29272  leopmul2i  29599  dvconstbi  40225  eel2131  40608  uun2131  40685  uun2131p1  40686  reccot  44359  rectan  44360
  Copyright terms: Public domain W3C validator