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

Theorem 3impdi 1452
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 660 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323impb 1136 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  oacan  7861  omcan  7882  ecovdi  8087  distrpi  10001  axltadd  10392  ccatlcan  13692  absmulgcd  15481  axlowdimlem14  26045  fh1  28801  fh2  28802  cm2j  28803  hoadddi  28986  hosubdi  28991  leopmul2i  29318  dvconstbi  39027  eel2131  39431  uun2131  39509  uun2131p1  39510  reccot  43064  rectan  43065
  Copyright terms: Public domain W3C validator