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

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

Proof of Theorem simpl11
StepHypRef Expression
1 simp11 1089 . 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  15459  tsmsxp  21881  brbtwn2  25702  ax5seg  25735  3vfriswmgr  27023  br8  31389  btwndiff  31811  ifscgr  31828  seglecgr12im  31894  lkrshp  33907  cvlcvr1  34141  atbtwn  34247  3dimlem3  34262  3dimlem3OLDN  34263  1cvratex  34274  llnmlplnN  34340  4atlem3  34397  4atlem3a  34398  4atlem11  34410  4atlem12  34413  lnatexN  34580  cdlemb  34595  paddasslem4  34624  paddasslem10  34630  pmodlem1  34647  llnexchb2lem  34669  llnexchb2  34670  arglem1N  34992  cdlemd4  35003  cdlemd9  35008  cdlemd  35009  cdleme16  35087  cdleme20  35127  cdleme21i  35138  cdleme21k  35141  cdleme27N  35172  cdleme28c  35175  cdlemefrs29bpre0  35199  cdlemefrs29clN  35202  cdlemefrs32fva  35203  cdleme41sn3a  35236  cdleme32fva  35240  cdleme40n  35271  cdlemg12e  35450  cdlemg15a  35458  cdlemg15  35459  cdlemg16ALTN  35461  cdlemg16z  35462  cdlemg20  35488  cdlemg22  35490  cdlemg29  35508  cdlemg38  35518  cdlemk33N  35712  cdlemk56  35774  dihord11b  36026  dihord2pre  36029  dihord4  36062  fourierdlem77  39733
  Copyright terms: Public domain W3C validator