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

Theorem simp32 1253
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp32 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜃)

Proof of Theorem simp32
StepHypRef Expression
1 simp2 1132 . 2 ((𝜒𝜃𝜏) → 𝜃)
213ad2ant3 1130 1 ((𝜑𝜓 ∧ (𝜒𝜃𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  simpl32OLD  1330  simpr32OLD  1348  simp132  1394  simp232  1403  simp332  1412  smogt  7633  axdc3lem4  9467  bitsfzo  15359  frlmphl  20322  mdetunilem4  20623  mdetuni0  20629  mdetmul  20631  decpmatmullem  20778  logfacbnd3  25147  logexprlim  25149  log2sumbnd  25432  ax5seg  26017  numclwlk1lem2foa  27513  iocinioc2  29850  totprob  30798  eqfunresadj  31966  nosupfv  32158  nosupres  32159  cgrtr  32405  cgrtr3  32407  ofscom  32420  cgrextend  32421  segconeq  32423  ifscgr  32457  colinearxfr  32488  brofs2  32490  brifs2  32491  fscgr  32493  btwnconn1lem2  32501  btwnconn1lem9  32508  btwnconn1lem10  32509  btwnconn1lem11  32510  btwnconn1lem12  32511  brsegle2  32522  seglecgr12im  32523  seglecgr12  32524  segletr  32527  outsideofeq  32543  ivthALT  32636  lshpkrlem5  34904  lshpkrlem6  34905  atbtwnexOLDN  35236  atbtwnex  35237  4noncolr3  35242  3dimlem3a  35249  3dim1  35256  3dim2  35257  1cvrat  35265  2atjlej  35268  hlatexch4  35270  ps-2b  35271  2atm  35316  ps-2c  35317  2atmat  35350  4atlem10  35395  4atlem11b  35397  4atlem11  35398  4at  35402  4at2  35403  2lplnja  35408  2lplnj  35409  dalemswapyz  35445  dalem-ddly  35475  cdlemb  35583  paddasslem5  35613  pmodlem1  35635  dalawlem1  35660  dalawlem3  35662  dalawlem4  35663  dalawlem5  35664  dalawlem6  35665  dalawlem7  35666  dalawlem8  35667  dalawlem9  35668  dalawlem11  35670  dalawlem12  35671  dalawlem15  35674  osumcllem5N  35749  osumcllem6N  35750  lhpexle3lem  35800  lhpmcvr4N  35815  lhpmcvr6N  35817  4atexlemex6  35863  4atex2  35866  4atex2-0bOLDN  35868  4atex2-0cOLDN  35869  ltrn11at  35936  trlval3  35977  cdlemd3  35990  cdleme7aa  36032  cdleme7b  36034  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme16aN  36049  cdleme11dN  36052  cdleme11e  36053  cdleme11l  36059  cdleme11  36060  cdleme12  36061  cdleme14  36063  cdleme15a  36064  cdleme15c  36066  cdleme16c  36070  cdleme16d  36071  cdleme16e  36072  cdleme16f  36073  cdleme17c  36078  cdleme18c  36083  cdlemeda  36088  cdlemednpq  36089  cdleme19a  36093  cdleme19c  36095  cdleme20aN  36099  cdleme20bN  36100  cdleme20l1  36110  cdleme20l2  36111  cdleme22aa  36129  cdleme22a  36130  cdleme22g  36138  cdleme23b  36140  cdleme23c  36141  cdleme26fALTN  36152  cdleme26f  36153  cdleme26f2ALTN  36154  cdleme26f2  36155  cdleme28b  36161  cdleme32b  36232  cdleme32c  36233  cdleme32e  36235  cdleme35h  36246  cdleme35sn2aw  36248  cdleme38m  36253  cdleme40n  36258  cdleme41sn3aw  36264  cdleme41sn4aw  36265  cdlemeg46gfre  36322  cdlemf1  36351  cdlemg1cex  36378  cdlemg2ce  36382  cdlemg4d  36403  cdlemg4  36407  cdlemg7fvN  36414  cdlemg8b  36418  cdlemg8c  36419  cdlemg9a  36422  cdlemg11aq  36428  cdlemg10a  36430  cdlemg12a  36433  cdlemg12b  36434  cdlemg12d  36436  cdlemg12g  36439  cdlemg12  36440  cdlemg13a  36441  cdlemg13  36442  cdlemg14f  36443  cdlemg14g  36444  cdlemg17b  36452  cdlemg17dN  36453  cdlemg17e  36455  cdlemg17pq  36462  cdlemg17iqN  36464  cdlemg18c  36470  cdlemg18d  36471  cdlemg19a  36473  cdlemg19  36474  cdlemg21  36476  cdlemg27a  36482  cdlemg28a  36483  cdlemg31b0N  36484  cdlemg27b  36486  cdlemg31c  36489  cdlemg33b0  36491  cdlemg28  36494  cdlemg33a  36496  cdlemg33  36501  cdlemg35  36503  cdlemg36  36504  cdlemg44a  36521  cdlemg46  36525  cdlemh2  36606  cdlemh  36607  cdlemj1  36611  cdlemk5  36626  cdlemk6  36627  cdlemki  36631  cdlemksv2  36637  cdlemk7  36638  cdlemk11  36639  cdlemkole  36643  cdlemk14  36644  cdlemk16  36647  cdlemk1u  36649  cdlemk18  36658  cdlemk19  36659  cdlemk7u  36660  cdlemk11u  36661  cdlemk33N  36699  cdlemkid2  36714  cdlemkfid3N  36715  cdlemk11ta  36719  cdlemk11tc  36735  cdlemk45  36737  cdlemk46  36738  cdlemk47  36739  cdlemk52  36744  cdlemk53a  36745  cdlemk54  36748  cdlemk55a  36749  cdleml1N  36766  cdleml3N  36768  cdlemn7  36994  cdlemn8  36995  cdlemn10  36997  dihordlem7  37005  dihordlem7b  37006  dihord1  37009  dihord10  37014  dihord11c  37015  dihord2  37018  hlhilphllem  37753  fmuldfeq  40318
  Copyright terms: Public domain W3C validator