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

Theorem 3impdi 1444
 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 908 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323impb 1108 1 ((𝜑𝜓𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072 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 197  df-an 385  df-3an 1074 This theorem is referenced by:  oacan  7799  omcan  7820  ecovdi  8024  distrpi  9932  axltadd  10323  ccatlcan  13692  absmulgcd  15488  axlowdimlem14  26055  fh1  28807  fh2  28808  cm2j  28809  hoadddi  28992  hosubdi  28997  leopmul2i  29324  dvconstbi  39053  eel2131  39459  uun2131  39538  uun2131p1  39539  reccot  43030  rectan  43031
 Copyright terms: Public domain W3C validator