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

Theorem simpl3l 1229
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpl3l (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl3l
StepHypRef Expression
1 simpll 766 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl3 1188 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  tfisi  7796  omopth2  8532  ltmul1a  12009  xaddass  13174  xlemul2a  13214  swrdsbslen  14558  swrdspsleq  14559  dvdsadd2b  16193  pockthg  16783  psgnunilem4  19284  efgred  19535  ptbasin  22944  basqtop  23078  xrsmopn  24191  nosupbnd1lem3  27074  nosupbnd1lem4  27075  noinfbnd1lem3  27089  noinfbnd1lem4  27090  noinfbnd1lem5  27091  axpasch  27932  axcontlem4  27958  elwwlks2ons3im  28941  br4  34387  btwnintr  34650  btwnexch3  34651  btwnouttr2  34653  cgrxfr  34686  lineext  34707  btwnconn1lem13  34730  btwnconn1lem14  34731  btwnconn3  34734  brsegle  34739  brsegle2  34740  segleantisym  34746  outsideofeu  34762  lineunray  34778  lineelsb2  34779  cvrcmp  37791  atcvrj2b  37941  3dimlem3  37970  3dimlem3OLDN  37971  3dim3  37978  ps-1  37986  lplnnle2at  38050  2llnm3N  38078  lvolnle3at  38091  4atlem0a  38102  4atlem3  38105  4atlem3a  38106  lnatexN  38288  paddasslem8  38336  paddasslem9  38337  paddasslem10  38338  paddasslem12  38340  paddasslem13  38341  lhp2lt  38510  lhpexle2lem  38518  lhpexle3  38521  lhpmcvr3  38534  lhpat3  38555  4atex  38585  trlval2  38672  ltrnideq  38684  ltrnatlw  38692  trlnle  38695  trlval4  38697  cdlemd4  38710  cdlemd5  38711  cdleme16  38794  cdleme21  38846  cdleme21k  38847  cdleme27cl  38875  cdleme27N  38878  cdleme29ex  38883  cdleme43fsv1snlem  38929  cdleme40m  38976  cdleme46f2g2  39002  cdleme46f2g1  39003  trlord  39078  cdlemg8  39140  cdlemg15a  39164  cdlemg16z  39168  cdlemg18a  39187  cdlemg24  39197  cdlemg38  39224  cdlemg40  39226  trlcone  39237  cdlemj2  39331  tendoid0  39334  tendoconid  39338  cdlemk34  39419  cdlemk38  39424  cdlemkid4  39443  cdlemk35s-id  39447  cdlemk39s-id  39449  cdlemk53  39466  tendospcanN  39532  cdlemm10N  39627  dihvalcqpre  39744  dihopelvalcpre  39757  dihord5b  39768  dihglblem5apreN  39800  dihmeetlem16N  39831  dihmeetlem17N  39832  dvh3dim3N  39958  qirropth  41274  mzpcong  41339  jm2.26  41369  aomclem6  41429  limcleqr  43971  fourierdlem42  44476  itsclc0b  46944
  Copyright terms: Public domain W3C validator