Theorem simp3l 1220

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

Assertion

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

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 488	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp13l  1307  simp23l  1313  simp33l  1319  tfisi  7859  fpr3g  8288  tfrlem5  8372  omeulem1  8573  omeulem2  8574  uniinqs  8801  elfiun  9404  tcrank  9870  isfin2-2  10325  konigthlem  10581  gruen  10825  addlid  11421  mulcan  11879  mulcan2  11880  divass  11918  divdir  11925  muldivdir  11935  subdivcomb1  11938  subdivcomb2  11939  divcan5  11945  ltmul1  12093  ltdiv1  12107  ltmuldiv  12116  lediv2  12133  xaddass2  13306  xlt2add  13316  xmulasslem3  13342  xadddi2  13353  expaddz  14174  expmulz  14176  muldivbinom2  14331  resqrtcl  15344  o1add  15705  o1mul  15706  o1sub  15707  dvdsadd2b  16402  dvdsgcd  16640  rpexp12i  16821  pythagtriplem3  16916  pcpremul  16941  pceu  16944  pcqmul  16951  pcqdiv  16955  setsstruct  17274  f1ocpbllem  17616  funcoppc  17970  funcres  17991  catcisolem  18205  1stfcl  18291  2ndfcl  18292  prfcl  18297  evlfcl  18316  curf1cl  18322  curfcl  18326  hofcl  18353  latjlej12  18549  latmlem12  18565  latj4  18583  latj4rot  18584  symgsssg  19600  symgfisg  19601  psgnunilem4  19630  odcong  19682  cmn4  19934  ablsub4  19943  abladdsub4  19944  lsm4  19993  abvdom  21002  abvres  21003  abvtrivd  21004  orngmul  21037  lspsolvlem  21335  lbsextlem2  21352  lidlsubcl  21418  frlmbas3  21995  matmulcell  22673  marrepeval  22791  ma1repveval  22799  submaeval  22810  mdetunilem3  22842  mdetuni0  22849  mdetmul  22851  minmar1eval  22877  nllyrest  23718  hausflimlem  24211  tsmsxp  24387  psmetlecl  24547  xmetlecl  24578  prdsxmetlem  24600  ngpocelbl  24936  bndth  25192  cph2ass  25447  iscau3  25512  dvres2  26146  coemullem  26483  vieta1  26551  aalioulem4  26578  cxpcn3lem  26992  angcan  27047  dchrvmasumlema  27744  logdivsum  27777  abvcxp  27859  padicabv  27874  nosupbnd1lem4  27955  nosupbnd1lem5  27956  noinfbnd1lem4  27970  cofcut1  28193  cofcut2  28195  divmulsw  28466  precsexlem8  28487  precsexlem9  28488  bdayfinbndlem1  28740  ax5seglem3  29396  ax5seglem6  29399  axpasch  29406  axeuclid  29428  axcontlem4  29432  axcontlem8  29436  wlkl1loop  30105  trlsonwlkon  30179  pthontrlon  30220  wspthsswwlknon  30397  umgr2cycllem  30633  umgr2cycl  30634  frgr2wwlkeqm  30819  adjlnop  32575  xreceu  33375  rhmdvd  33772  measvunilem  34731  measvunilem0  34732  measres  34741  bnj1128  35507  satfv1fvfmla1  36010  cgrcomim  36577  cgrcoml  36584  cgrcomr  36585  cgrdegen  36592  segconeu  36599  btwnintr  36607  btwnexch3  36608  btwnouttr2  36610  btwnouttr  36612  btwnexch  36613  trisegint  36616  lineext  36664  linecgr  36669  lineid  36671  idinside  36672  btwnconn1lem3  36677  btwnconn1lem4  36678  btwnconn1lem7  36681  btwnconn1lem14  36688  btwnconn2  36690  midofsegid  36692  btwnoutside  36713  outsideoftr  36717  lineunray  36735  lineelsb2  36736  cnres2  38521  heibor  38579  lsmcv2  39910  lcvat  39911  lcvexchlem4  39918  lcvexchlem5  39919  lfladd  39947  lflsub  39948  lflmul  39949  lshpkrlem4  39994  latm4  40114  omlmod1i2N  40141  cvlatexch3  40219  cvlsupr7  40229  hlatj4  40255  hlrelat3  40293  cvrval3  40294  atcvrj1  40312  atlelt  40319  2atlt  40320  2atjm  40326  3noncolr2  40330  athgt  40337  3dimlem2  40340  3dimlem4  40345  3dimlem4OLDN  40346  3dim3  40350  1cvratex  40354  ps-1  40358  ps-2  40359  hlatexch3N  40361  llnle  40399  atcvrlln2  40400  atcvrlln  40401  lplni2  40418  lplnle  40421  lplnnle2at  40422  llncvrlpln2  40438  lplnexllnN  40445  2llnmeqat  40452  lvolnle3at  40463  4atlem0ae  40475  lplncvrlvol2  40496  lnjatN  40661  lncvrat  40663  cdlemblem  40674  elpaddri  40683  paddasslem2  40702  paddasslem16  40716  padd4N  40721  hlmod1i  40737  dalawlem2  40753  pclfinN  40781  pexmidlem4N  40854  pl42lem1N  40860  lhp2lt  40882  lhpexle1  40889  lhpexle2lem  40890  lhpj1  40903  lhpmcvr5N  40908  lhp2at0  40913  lhp2atnle  40914  lhp2at0nle  40916  lhple  40923  lhpat  40924  lhpat4N  40925  4atexlempnq  40936  4atexlem7  40956  4atex  40957  ltrn11  41007  ltrnle  41010  ltrnm  41012  ltrnj  41013  ltrncvr  41014  ltrnel  41020  ltrncnvel  41023  ltrncnv  41027  trlval2  41044  trlcnv  41046  trljat1  41047  trljat2  41048  trlat  41050  trl0  41051  trlnidat  41054  trlnid  41060  cdlemc1  41072  cdlemc2  41073  cdlemc5  41076  cdlemd2  41080  cdlemd7  41085  cdlemd8  41086  cdlemd9  41087  cdleme0e  41098  cdleme3g  41115  cdleme3h  41116  cdleme3  41118  cdleme5  41121  cdleme10  41135  cdleme11a  41141  cdleme11c  41142  cdleme11h  41147  cdleme11j  41148  cdleme0nex  41171  cdleme18a  41172  cdleme18b  41173  cdleme22gb  41175  cdleme20zN  41182  cdleme20c  41192  cdleme20k  41200  cdleme21a  41206  cdleme21b  41207  cdleme21c  41208  cdleme21h  41215  cdleme22b  41222  cdleme22d  41224  cdleme22f  41227  cdleme25a  41234  cdleme25c  41236  cdleme25dN  41237  cdleme26ee  41241  cdleme30a  41259  cdlemefr29bpre0N  41287  cdlemefr29clN  41288  cdlemefr32fvaN  41290  cdlemefr32fva1  41291  cdlemefs29bpre0N  41297  cdlemefs29bpre1N  41298  cdlemefs29cpre1N  41299  cdlemefs29clN  41300  cdleme43fsv1snlem  41301  cdlemefs32fvaN  41303  cdlemefs32fva1  41304  cdlemefs31fv1  41305  cdleme36a  41341  cdleme39a  41346  cdleme42a  41352  cdleme42c  41353  cdleme17d3  41377  cdleme48fv  41380  cdleme48bw  41383  cdleme48b  41384  cdlemeg46rgv  41409  cdlemeg46req  41410  cdlemeg46gfv  41411  cdleme48d  41416  cdleme50trn2a  41431  cdleme50trn2  41432  cdleme50ltrn  41438  cdlemf1  41442  cdlemf  41444  trlord  41450  cdlemg2dN  41471  cdlemg2fvlem  41475  cdlemg2l  41484  cdlemg7fvbwN  41488  cdlemg7aN  41506  cdlemg10bALTN  41517  cdlemg10c  41520  cdlemg17a  41542  cdlemg17dALTN  41545  cdlemg31b0a  41576  cdlemg31a  41578  cdlemg31b  41579  cdlemg34  41593  cdlemg36  41595  ltrnco  41600  trlcoabs2N  41603  trlcolem  41607  cdlemg48  41618  tgrpov  41629  tendoco2  41649  tendoplco2  41660  cdlemh1  41696  cdlemi1  41699  cdlemi2  41700  cdlemj3  41704  tendoid0  41706  cdlemk1  41712  cdlemk2  41713  cdlemk4  41715  cdlemk8  41719  cdlemk9  41720  cdlemk9bN  41721  cdlemk10  41724  cdlemk26b-3  41786  cdlemk26-3  41787  cdlemk28-3  41789  cdlemk37  41795  cdlemk39  41797  cdlemkfid1N  41802  cdlemkid1  41803  cdlemky  41807  cdlemkyu  41808  cdlemk19ylem  41811  cdlemk19xlem  41823  cdlemk11t  41827  cdlemk51  41834  cdlemkyyN  41843  cdleml6  41862  cdleml7  41863  cdleml8  41864  cdleml9  41865  erngdvlem4  41872  erngdvlem4-rN  41880  tendospcanN  41904  dia11N  41929  cdlemm10N  41999  dib11N  42041  dicvaddcl  42071  dicvscacl  42072  cdlemn6  42083  dihvalcq2  42128  dihopelvalcpre  42129  dihord6b  42141  dihord5apre  42143  dihmeetlem1N  42171  dihmeetlem2N  42180  dihglbcpreN  42181  dihjatc1  42192  dihmeetlem20N  42207  dih1dimatlem0  42209  dihatlat  42215  dihglblem6  42221  dochexmidlem4  42344  mapdpglem32  42586  mapdh8ad  42660  mapdh9aOLDN  42671  hdmap11lem2  42723  hdmap14lem6  42754  frlmfzowrdb  43400  flt4lem5  43504  mzpsubst  43601  pellex  43684  pellfundex  43735  pellfund14gap  43736  qirropth  43757  rmxypos  43796  congmul  43816  congsub  43819  mzpcong  43821  coprmdvdsb  43834  jm2.15nn0  43852  jm2.16nn0  43853  rpnnen3lem  43880  idomsubgmo  44042  relexp01min  44561  mullimc  46454  islptre  46457  limccog  46458  mullimcf  46461  addlimc  46484  0ellimcdiv  46485  limsupre3lem  46568  stoweidlem57  46893  fourierdlem48  46990  fourierdlem80  47022  fourierdlem113  47055  ovncvrrp  47400  opnvonmbllem2  47469  ovolval5lem3  47490  ovnovollem3  47494  grlimedgclnbgr  48919  itsclc0lem1  49694  itsclc0lem2  49695  itschlc0yqe  49698  itscnhlc0xyqsol  49703  itschlc0xyqsol1  49704  swapffunc  50216  fucofunc  50293  fucoppc  50344