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

Theorem 3impdi 1349
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 1114 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 1088
This theorem is referenced by:  oacan  8585  omcan  8606  ecovdi  8864  distrpi  10936  axltadd  11332  ccatlcan  14753  absmulgcd  16583  axlowdimlem14  28985  fh1  31647  fh2  31648  cm2j  31649  hoadddi  31832  hosubdi  31837  leopmul2i  32164  dvconstbi  44330  eel2131  44712  uun2131  44789  uun2131p1  44790  io1ii  48717  reccot  48989  rectan  48990
  Copyright terms: Public domain W3C validator