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

Theorem simpl3l 1222
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 763 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl3 1181 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  tfisi  7564  omopth2  8203  ltmul1a  11481  xaddass  12635  xlemul2a  12675  swrdsbslen  14019  swrdspsleq  14020  dvdsadd2b  15648  pockthg  16234  psgnunilem4  18547  efgred  18796  ptbasin  22101  basqtop  22235  xrsmopn  23335  axpasch  26641  axcontlem4  26667  elwwlks2ons3im  27647  br4  32878  nosupbnd1lem3  33094  nosupbnd1lem4  33095  btwnintr  33364  btwnexch3  33365  btwnouttr2  33367  cgrxfr  33400  lineext  33421  btwnconn1lem13  33444  btwnconn1lem14  33445  btwnconn3  33448  brsegle  33453  brsegle2  33454  segleantisym  33460  outsideofeu  33476  lineunray  33492  lineelsb2  33493  cvrcmp  36286  atcvrj2b  36435  3dimlem3  36464  3dimlem3OLDN  36465  3dim3  36472  ps-1  36480  lplnnle2at  36544  2llnm3N  36572  lvolnle3at  36585  4atlem0a  36596  4atlem3  36599  4atlem3a  36600  lnatexN  36782  paddasslem8  36830  paddasslem9  36831  paddasslem10  36832  paddasslem12  36834  paddasslem13  36835  lhp2lt  37004  lhpexle2lem  37012  lhpexle3  37015  lhpmcvr3  37028  lhpat3  37049  4atex  37079  trlval2  37166  ltrnideq  37178  ltrnatlw  37186  trlnle  37189  trlval4  37191  cdlemd4  37204  cdlemd5  37205  cdleme16  37288  cdleme21  37340  cdleme21k  37341  cdleme27cl  37369  cdleme27N  37372  cdleme29ex  37377  cdleme43fsv1snlem  37423  cdleme40m  37470  cdleme46f2g2  37496  cdleme46f2g1  37497  trlord  37572  cdlemg8  37634  cdlemg15a  37658  cdlemg16z  37662  cdlemg18a  37681  cdlemg24  37691  cdlemg38  37718  cdlemg40  37720  trlcone  37731  cdlemj2  37825  tendoid0  37828  tendoconid  37832  cdlemk34  37913  cdlemk38  37918  cdlemkid4  37937  cdlemk35s-id  37941  cdlemk39s-id  37943  cdlemk53  37960  tendospcanN  38026  cdlemm10N  38121  dihvalcqpre  38238  dihopelvalcpre  38251  dihord5b  38262  dihglblem5apreN  38294  dihmeetlem16N  38325  dihmeetlem17N  38326  dvh3dim3N  38452  qirropth  39366  mzpcong  39430  jm2.26  39460  aomclem6  39520  limcleqr  41786  fourierdlem42  42296  itsclc0b  44587
  Copyright terms: Public domain W3C validator