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

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

Proof of Theorem simpl2r
StepHypRef Expression
1 simplr 785 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜓)
213ad2antl2 1237 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:  soisores  6768  omopth2  7868  fin23lem11  9391  xmulasslem3  12317  ssfzo12bi  12770  ntrivcvgmul  14918  pockthg  15890  gsmsymgreqlem2  18115  efgred  18426  lspfixed  19399  lspfixedOLD  19400  decpmatmullem  20854  decpmatmul  20855  unconn  21511  llyrest  21567  basqtop  21793  tmdgsum  22177  tsmsxp  22236  ucncn  22367  mulcxp  24721  cxple2  24733  ax5seglem1  26098  ax5seglem2  26099  axpasch  26111  axcontlem4  26137  1pthon2v  27388  cvmlift2lem10  31673  br4  32024  cgrcomim  32471  btwnintr  32501  btwnouttr2  32504  btwndiff  32509  btwnconn1lem14  32582  btwnconn3  32585  segcon2  32587  brsegle  32590  brsegle2  32591  segleantisym  32597  outsideofeu  32613  eqlkr  34987  eqlkr2  34988  lkrlsp  34990  atbtwn  35334  3dimlem3OLDN  35350  3dim3  35357  3atlem7  35377  4atlem0a  35481  4atlem3a  35485  4atlem11  35497  lneq2at  35666  lnatexN  35667  paddasslem6  35713  llnexchb2  35757  lhpexle2lem  35897  lhpexle3  35900  lhp2at0nle  35923  lhpat3  35934  trlnid  36067  ltrneq3  36096  cdleme17b  36175  cdleme27cl  36254  cdlemefrs29bpre0  36284  cdlemefrs29clN  36287  cdlemefrs32fva  36288  cdlemefs32sn1aw  36302  cdleme32le  36335  ltrniotavalbN  36472  cdlemg6  36511  cdlemg7N  36514  cdlemg11b  36530  cdlemg15a  36543  cdlemg15  36544  cdlemg39  36604  trlcone  36616  cdlemg42  36617  tendoconid  36717  tendotr  36718  cdlemk39u  36856  cdlemk19u  36858  tendoex  36863  cdlemm10N  37006  dihord2pre  37113  dihord4  37146  dihord5b  37147  dihglbcpreN  37188  dihmeetlem13N  37207  dih1dimatlem0  37216  mzpcong  38148  jm2.25lem1  38174  jm2.26  38178  idomsubgmo  38385
  Copyright terms: Public domain W3C validator