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

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

Proof of Theorem simpl3r
StepHypRef Expression
1 simplr 767 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl3 1187 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  tfisi  7800  offsplitfpar  8056  omopth2  8536  ltmul1a  12013  xmulasslem3  13215  xadddi2  13226  swrdsbslen  14564  swrdspsleq  14565  dvdsadd2b  16199  pockthg  16789  psgnunilem4  19293  efgred  19544  marrepeval  21949  submaeval  21968  mdetmul  22009  minmar1eval  22035  ptbasin  22965  basqtop  23099  xrsmopn  24212  nosupbnd1lem3  27095  nosupbnd1lem4  27096  nosupbnd1lem5  27097  noinfbnd1lem3  27110  noinfbnd1lem4  27111  noinfbnd1lem5  27112  axpasch  27953  axeuclid  27975  elwwlks2ons3im  28962  br4  34417  btwnouttr2  34683  trisegint  34689  cgrxfr  34716  lineext  34737  btwnconn1lem13  34760  btwnconn1lem14  34761  btwnconn3  34764  brsegle  34769  brsegle2  34770  segleantisym  34776  outsideofeu  34792  lineunray  34808  lineelsb2  34809  cvrcmp  37818  atcvrj2b  37968  3dimlem3  37997  3dimlem3OLDN  37998  3dim3  38005  ps-1  38013  ps-2  38014  lplnnle2at  38077  2llnm3N  38105  4atlem0a  38129  4atlem3  38132  4atlem3a  38133  lnatexN  38315  paddasslem8  38363  paddasslem9  38364  paddasslem10  38365  paddasslem12  38367  paddasslem13  38368  lhpexle2lem  38545  lhpexle3  38548  lhpat3  38582  4atex  38612  trlval2  38699  trlval4  38724  cdleme16  38821  cdleme21  38873  cdleme21k  38874  cdleme27cl  38902  cdleme27N  38905  cdleme43fsv1snlem  38956  cdleme48fvg  39036  cdlemg8  39167  cdlemg15a  39191  cdlemg16z  39195  cdlemg24  39224  cdlemg38  39251  cdlemg40  39253  trlcone  39264  cdlemj2  39358  tendoid0  39361  tendoconid  39365  cdlemk34  39446  cdlemk38  39451  cdlemkid4  39470  cdlemk53  39493  tendospcanN  39559  dihvalcqpre  39771  dihmeetlem15N  39857  qirropth  41289  mzpcong  41354  jm2.26  41384  aomclem6  41444  islptre  43980  limccog  43981  limcleqr  44005  fourierdlem42  44510  elaa2  44595  itsclc0b  46978
  Copyright terms: Public domain W3C validator