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

Theorem simpl3l 1301
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 783 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl3 1238 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  tfisi  7255  omopth2  7868  ltmul1a  11125  xaddass  12280  xlemul2a  12320  swrdsbslen  13649  dvdsadd2b  15314  pockthg  15890  psgnunilem4  18182  efgred  18426  ptbasin  21659  basqtop  21793  xrsmopn  22893  axpasch  26111  axcontlem4  26137  elwwlks2ons3im  27156  br4  32024  nosupbnd1lem3  32231  nosupbnd1lem4  32232  btwnintr  32501  btwnexch3  32502  btwnouttr2  32504  cgrxfr  32537  lineext  32558  btwnconn1lem13  32581  btwnconn1lem14  32582  btwnconn3  32585  brsegle  32590  brsegle2  32591  segleantisym  32597  outsideofeu  32613  lineunray  32629  lineelsb2  32630  cvrcmp  35171  atcvrj2b  35320  3dimlem3  35349  3dimlem3OLDN  35350  3dim3  35357  ps-1  35365  lplnnle2at  35429  2llnm3N  35457  lvolnle3at  35470  4atlem0a  35481  4atlem3  35484  4atlem3a  35485  lnatexN  35667  paddasslem8  35715  paddasslem9  35716  paddasslem10  35717  paddasslem12  35719  paddasslem13  35720  lhp2lt  35889  lhpexle2lem  35897  lhpexle3  35900  lhpmcvr3  35913  lhpat3  35934  4atex  35964  trlval2  36051  ltrnideq  36063  ltrnatlw  36071  trlnle  36074  trlval4  36076  cdlemd4  36089  cdlemd5  36090  cdleme16  36173  cdleme21  36225  cdleme21k  36226  cdleme27cl  36254  cdleme27N  36257  cdleme29ex  36262  cdleme43fsv1snlem  36308  cdleme40m  36355  cdleme46f2g2  36381  cdleme46f2g1  36382  trlord  36457  cdlemg8  36519  cdlemg15a  36543  cdlemg16z  36547  cdlemg18a  36566  cdlemg24  36576  cdlemg38  36603  cdlemg40  36605  trlcone  36616  cdlemj2  36710  tendoid0  36713  tendoconid  36717  cdlemk34  36798  cdlemk38  36803  cdlemkid4  36822  cdlemk35s-id  36826  cdlemk39s-id  36828  cdlemk53  36845  tendospcanN  36911  cdlemm10N  37006  dihvalcqpre  37123  dihopelvalcpre  37136  dihord5b  37147  dihglblem5apreN  37179  dihmeetlem16N  37210  dihmeetlem17N  37211  dvh3dim3N  37337  qirropth  38082  mzpcong  38148  jm2.26  38178  aomclem6  38238  limcleqr  40446  fourierdlem42  40935
  Copyright terms: Public domain W3C validator