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

Theorem simpl12 1135
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl12 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl12
StepHypRef Expression
1 simp12 1090 . 2 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜓)
21adantr 481 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  pythagtriplem4  15448  pmatcollpw1lem1  20498  pmatcollpw1  20500  mp2pm2mplem2  20531  brbtwn2  25685  ax5seg  25718  3vfriswmgr  27006  br8  31351  ifscgr  31790  seglecgr12im  31856  lkrshp  33869  atlatle  34084  cvlcvr1  34103  atbtwn  34209  3dimlem3  34224  3dimlem3OLDN  34225  1cvratex  34236  llnmlplnN  34302  4atlem3  34359  4atlem3a  34360  4atlem11  34372  4atlem12  34375  cdlemb  34557  paddasslem4  34586  paddasslem10  34592  pmodlem1  34609  llnexchb2lem  34631  arglem1N  34954  cdlemd4  34965  cdlemd  34971  cdleme16  35049  cdleme20  35089  cdleme21k  35103  cdleme22cN  35107  cdleme27N  35134  cdleme28c  35137  cdleme29ex  35139  cdleme32fva  35202  cdleme40n  35233  cdlemg15a  35420  cdlemg15  35421  cdlemg16ALTN  35423  cdlemg16z  35424  cdlemg20  35450  cdlemg22  35452  cdlemg29  35470  cdlemg38  35480  cdlemk33N  35674  cdlemk56  35736  fourierdlem77  39704
  Copyright terms: Public domain W3C validator