Theorem simp1l 1199

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1l	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1134	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp11l  1286  simp21l  1292  simp31l  1298  2f1fvneq  7218  eqfunresadj  7318  tfisi  7813  offsplitfpar  8073  poseq  8112  omeulem2  8522  uniinqs  8748  unxpdomlem3  9172  elfiun  9347  cantnffval  9586  tcrank  9810  cofsmo  10193  isfin2-2  10243  tskint  10710  tskun  10711  tskurn  10714  gruina  10743  dedekind  11310  subaddmulsub  11614  dmdcan  11865  lt2msq1  12040  supmullem1  12126  supmul  12128  xaddass  13178  xaddass2  13179  xlt2add  13189  xmulasslem3  13215  xadddi2r  13227  iccsplit  13415  expaddzlem  14042  expaddz  14043  expmulz  14045  ccatopth2  14654  pfxccat3  14671  resqrtcl  15190  limsupgle  15414  o1add  15551  o1mul  15552  o1sub  15553  bitsfzo  16376  sadfval  16393  smufval  16418  nn0rppwr  16502  prmexpb  16660  4sqlem18  16904  vdwlem10  16932  fsets  17110  setsstruct2  17115  submre  17538  mrelatlub  18499  chnccat  18563  gsmsymgreqlem2  19377  mndodcong  19488  subgabl  19782  gex2abl  19797  ogrpinvlt  20090  cntzsubrng  20517  cntzsubr  20556  abvres  20781  lbsind2  21050  lspsneu  21095  lbsextlem2  21131  lbsextg  21134  lindfind2  21790  matring  22404  maducoeval  22600  maducoeval2  22601  maduf  22602  madurid  22605  gsummatr01  22620  cramerimplem3  22646  cnprest  23250  hausnei2  23314  isreg2  23338  cmpcld  23363  llyrest  23446  nllyrest  23447  csdfil  23855  hausflimlem  23940  ssblps  24383  ssbl  24384  cphassi  25187  cphassir  25188  4cphipval2  25215  cphipval  25216  dvres2  25886  plyadd  26195  plymul  26196  coeeu  26203  vieta1  26293  aalioulem3  26315  aalioulem4  26316  efgh  26523  cxpadd  26661  cxpsub  26664  mulcxp  26667  divcxp  26669  cxple2  26679  cxplt2  26680  cxpcn3lem  26730  angcan  26785  ang180lem5  26796  isosctrlem3  26803  logexprlim  27209  lgssq  27321  abvcxp  27599  padicabv  27614  nosupbnd2lem1  27700  noinfbnd2lem1  27715  nosupinfsep  27717  noetalem1  27726  ltmuls2  28184  brbtwn2  28996  ax5seglem6  29025  axcontlem4  29058  axcontlem8  29062  uhgr2edg  29299  nbgrisvtx  29432  nbupgrres  29455  clwwlkccat  30083  clwwlknonex2lem2  30201  frgrreggt1  30486  chscllem4  31734  cshwrnid  33060  ifscgr  36266  matunitlindflem1  37896  lshpnelb  39389  lfl1  39475  lshpkrlem6  39520  lshpkrex  39523  hlrelat3  39817  atbtwnexOLDN  39852  atbtwnex  39853  3dim3  39874  3atlem5  39892  2llnmat  39929  lvolex3N  39943  lvolnle3at  39987  4atlem11  40014  4atlem12  40017  dalemccea  40088  cdlema2N  40197  paddasslem2  40226  atmod1i1m  40263  lhp2lt  40406  lhp0lt  40408  lhpj1  40427  lhpmcvr4N  40431  lhpelim  40442  lhpmod2i2  40443  lhpmod6i1  40444  cdlemb2  40446  lhple  40447  lhpat  40448  4atex  40481  4atex2-0aOLDN  40483  4atex3  40486  ldilco  40521  ltrncl  40530  ltrn11  40531  ltrnle  40534  ltrncnvleN  40535  ltrnm  40536  ltrnj  40537  ltrncvr  40538  ltrnatb  40542  ltrnel  40544  ltrncnvel  40547  ltrncnv  40551  trlval2  40568  trlcnv  40570  trljat1  40571  trljat2  40572  trl0  40575  ltrnnidn  40579  trlnidatb  40582  cdlemc1  40596  cdlemc2  40597  cdlemc5  40600  cdlemc6  40601  cdlemd3  40605  cdlemd6  40608  cdleme0aa  40615  cdleme0b  40617  cdleme0c  40618  cdleme0e  40622  cdleme0fN  40623  cdleme01N  40626  cdleme02N  40627  cdleme0ex1N  40628  cdleme0moN  40630  cdleme3g  40639  cdleme3h  40640  cdleme3  40642  cdleme4  40643  cdleme4a  40644  cdleme5  40645  cdleme8  40655  cdleme9  40658  cdleme10  40659  cdleme16aN  40664  cdleme11a  40665  cdleme11fN  40669  cdleme11g  40670  cdleme11h  40671  cdleme11j  40672  cdleme11k  40673  cdleme12  40676  cdleme13  40677  cdleme17c  40693  cdleme17d1  40694  cdleme18a  40696  cdleme18b  40697  cdleme18c  40698  cdleme22gb  40699  cdlemeda  40703  cdlemednpq  40704  cdlemednuN  40705  cdleme19c  40710  cdleme20aN  40714  cdleme20bN  40715  cdleme20c  40716  cdleme22aa  40744  cdleme22a  40745  cdleme22b  40746  cdleme22d  40748  cdleme22e  40749  cdleme27cl  40771  cdleme27a  40772  cdleme30a  40783  cdleme42a  40876  cdleme42c  40877  cdleme50laut  40952  cdlemf1  40966  cdlemf  40968  cdlemfnid  40969  trlord  40974  cdlemg2fv2  41005  cdlemg2kq  41007  cdlemg2m  41009  cdlemg4a  41013  cdlemg4d  41018  cdlemg4g  41021  cdlemg4  41022  cdlemg6c  41025  cdlemg7aN  41030  cdlemg8a  41032  cdlemg8b  41033  cdlemg8c  41034  cdlemg9a  41037  cdlemg9b  41038  cdlemg9  41039  cdlemg11aq  41043  cdlemg10c  41044  cdlemg12a  41048  cdlemg12b  41049  cdlemg12c  41050  cdlemg17a  41066  cdlemg18b  41084  cdlemg18c  41085  cdlemg31b0a  41100  cdlemg31a  41102  cdlemg31b  41103  cdlemg31d  41105  cdlemg35  41118  trlcoabs2N  41127  trlcolem  41131  cdlemg44a  41136  trljco  41145  trljco2  41146  tendoco2  41173  tendopltp  41185  cdlemi1  41223  cdlemi2  41224  cdlemj3  41228  tendocan  41229  cdlemk3  41238  cdlemk4  41239  cdlemk5a  41240  cdlemk9  41244  cdlemk9bN  41245  cdlemkvcl  41247  cdlemk10  41248  cdlemk30  41299  cdlemk31  41301  cdlemk39  41321  cdlemkfid1N  41326  cdlemkid1  41327  cdlemkid2  41329  cdlemkfid3N  41330  cdlemk19ylem  41335  cdlemk19xlem  41347  cdlemk19x  41348  cdlemk53b  41361  cdlemk53  41362  cdlemk54  41363  cdlemk55a  41364  cdlemk43N  41368  cdlemk19u1  41374  cdlemk19u  41375  cdleml1N  41381  erngdvlem4  41396  erngdvlem4-rN  41404  dia11N  41453  cdlemm10N  41523  dib11N  41565  cdlemn2  41600  cdlemn10  41611  dihjustlem  41621  dihord2cN  41626  dihlsscpre  41639  dih1dimb2  41646  dihvalcq2  41652  dihopelvalcpre  41653  dihord6b  41665  dih11  41670  dihmeetlem1N  41695  dihglblem2N  41699  dihglblem3N  41700  dihmeetlem2N  41704  dihglbcpreN  41705  dihmeetcN  41707  dihmeetbclemN  41709  dihmeetlem4preN  41711  dihmeetlem9N  41720  dihmeetlem20N  41731  dihlspsnssN  41737  dihlspsnat  41738  dihatlat  41739  dihglblem6  41745  dihmeet  41748  dochss  41770  hdmapval3N  42243  hgmap11  42307  remulcand  42838  congtr  43351  fzmaxdif  43367  isnumbasgrplem2  43490  ntrclsk13  44456  ssmapsn  45603  infleinf  45759  suplesup2  45763  supxrunb3  45786  mullimc  46005  mullimcf  46012  islpcn  46026  limsupresxr  46153  liminfresxr  46154  cncfuni  46273  icccncfext  46274  stoweidlem34  46421  stoweidlem59  46446  stirlinglem13  46473  fourierdlem41  46535  fourierdlem42  46536  fourierdlem73  46566  sge0iunmptlemfi  46800  meadjiunlem  46852  ovncvrrp  46951  sssmf  47125  smflimsuplem7  47213  smflimsuplem8  47214  ormkglobd  47262  funressneu  47436  grlimedgclnbgr  48384  lincscm  48819  lincext3  48845  el0ldep  48855  el0ldepsnzr  48856  itscnhlc0xyqsol  49154  uptr2  49609