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

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

Proof of Theorem simpl11
StepHypRef Expression
1 simp11 1222 . 2 (((𝜑𝜓𝜒) ∧ 𝜃𝜏) → 𝜑)
21adantr 472 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:  pythagtriplem4  15647  tsmsxp  22080  brbtwn2  25905  ax5seg  25938  3vfriswmgr  27353  br8  31874  nolt02o  32072  btwndiff  32361  ifscgr  32378  seglecgr12im  32444  lkrshp  34812  cvlcvr1  35046  atbtwn  35152  3dimlem3  35167  3dimlem3OLDN  35168  1cvratex  35179  llnmlplnN  35245  4atlem3  35302  4atlem3a  35303  4atlem11  35315  4atlem12  35318  lnatexN  35485  cdlemb  35500  paddasslem4  35529  paddasslem10  35535  pmodlem1  35552  llnexchb2lem  35574  llnexchb2  35575  arglem1N  35897  cdlemd4  35908  cdlemd9  35913  cdlemd  35914  cdleme16  35992  cdleme20  36031  cdleme21i  36042  cdleme21k  36045  cdleme27N  36076  cdleme28c  36079  cdlemefrs29bpre0  36103  cdlemefrs29clN  36106  cdlemefrs32fva  36107  cdleme41sn3a  36140  cdleme32fva  36144  cdleme40n  36175  cdlemg12e  36354  cdlemg15a  36362  cdlemg15  36363  cdlemg16ALTN  36365  cdlemg16z  36366  cdlemg20  36392  cdlemg22  36394  cdlemg29  36412  cdlemg38  36422  cdlemk33N  36616  cdlemk56  36678  dihord11b  36930  dihord2pre  36933  dihord4  36966  fourierdlem77  40820
  Copyright terms: Public domain W3C validator