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

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

Proof of Theorem simpl13
StepHypRef Expression
1 simp13 1092 . 2 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜒)
21adantr 481 1 ((((𝜑𝜓𝜒) ∧ 𝜃𝜏) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037
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 1039
This theorem is referenced by:  pythagtriplem4  15518  mply1topmatcl  20604  brbtwn2  25779  ax5seg  25812  br8  31632  nolt02o  31829  btwndiff  32118  ifscgr  32135  seglecgr12im  32201  atlatle  34433  cvlcvr1  34452  atbtwn  34558  3dimlem3  34573  3dimlem3OLDN  34574  4atlem3  34708  4atlem11  34721  4atlem12  34724  2lplnj  34732  paddasslem4  34935  paddasslem10  34941  pmodlem1  34958  llnexchb2lem  34980  pclfinclN  35062  arglem1N  35303  cdlemd4  35314  cdlemd  35320  cdleme16  35398  cdleme20  35438  cdleme21k  35452  cdleme22cN  35456  cdleme27N  35483  cdleme28c  35486  cdleme29ex  35488  cdleme32fva  35551  cdleme40n  35582  cdlemg15a  35769  cdlemg15  35770  cdlemg16ALTN  35772  cdlemg16z  35773  cdlemg20  35799  cdlemg22  35801  cdlemg29  35819  cdlemg38  35829  cdlemk56  36085  dihord2pre  36340  uzwo4  39047  fourierdlem77  40169
  Copyright terms: Public domain W3C validator