Theorem simp3l 1208

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 483	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1141	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp13l  1295  simp23l  1301  simp33l  1307  tfisi  7806  fpr3g  8232  tfrlem5  8316  omeulem1  8514  omeulem2  8515  uniinqs  8741  elfiun  9340  tcrank  9806  isfin2-2  10239  konigthlem  10489  gruen  10733  addlid  11327  mulcan  11785  mulcan2  11786  divass  11825  divdir  11832  div11OLD  11836  muldivdir  11845  subdivcomb1  11848  subdivcomb2  11849  divcan5  11855  ltmul1  12003  ltdiv1  12018  ltmuldiv  12027  lediv2  12044  xaddass2  13200  xlt2add  13210  xmulasslem3  13236  xadddi2  13247  expaddz  14066  expmulz  14068  muldivbinom2  14223  resqrtcl  15213  o1add  15574  o1mul  15575  o1sub  15576  dvdsadd2b  16273  dvdsgcd  16511  rpexp12i  16692  pythagtriplem3  16787  pcpremul  16812  pceu  16815  pcqmul  16822  pcqdiv  16826  setsstruct  17144  f1ocpbllem  17486  funcoppc  17840  funcres  17861  catcisolem  18075  1stfcl  18161  2ndfcl  18162  prfcl  18167  evlfcl  18186  curf1cl  18192  curfcl  18196  hofcl  18223  latjlej12  18419  latmlem12  18435  latj4  18453  latj4rot  18454  symgsssg  19440  symgfisg  19441  psgnunilem4  19470  odcong  19522  cmn4  19774  ablsub4  19783  abladdsub4  19784  lsm4  19833  abvdom  20809  abvres  20810  abvtrivd  20811  orngmul  20844  lspsolvlem  21142  lbsextlem2  21159  lidlsubcl  21224  frlmbas3  21758  matmulcell  22435  marrepeval  22553  ma1repveval  22561  submaeval  22572  mdetunilem3  22604  mdetuni0  22611  mdetmul  22613  minmar1eval  22639  nllyrest  23476  hausflimlem  23969  tsmsxp  24145  psmetlecl  24305  xmetlecl  24336  prdsxmetlem  24358  ngpocelbl  24694  bndth  24950  cph2ass  25205  iscau3  25270  dvres2  25904  coemullem  26240  vieta1  26303  aalioulem4  26326  cxpcn3lem  26736  angcan  26791  dchrvmasumlema  27488  logdivsum  27521  abvcxp  27603  padicabv  27618  nosupbnd1lem4  27700  nosupbnd1lem5  27701  noinfbnd1lem4  27715  cofcut1  27937  cofcut2  27939  divmulsw  28210  precsexlem8  28231  precsexlem9  28232  bdayfinbndlem1  28484  ax5seglem3  29025  ax5seglem6  29028  axpasch  29035  axeuclid  29057  axcontlem4  29061  axcontlem8  29065  wlkl1loop  29731  trlsonwlkon  29801  pthontrlon  29840  wspthsswwlknon  30014  frgr2wwlkeqm  30426  adjlnop  32182  xreceu  33007  rhmdvd  33414  measvunilem  34403  measvunilem0  34404  measres  34413  bnj1128  35179  umgr2cycllem  35375  umgr2cycl  35376  satfv1fvfmla1  35658  cgrcomim  36224  cgrcoml  36231  cgrcomr  36232  cgrdegen  36239  segconeu  36246  btwnintr  36254  btwnexch3  36255  btwnouttr2  36257  btwnouttr  36259  btwnexch  36260  trisegint  36263  lineext  36311  linecgr  36316  lineid  36318  idinside  36319  btwnconn1lem3  36324  btwnconn1lem4  36325  btwnconn1lem7  36328  btwnconn1lem14  36335  btwnconn2  36337  midofsegid  36339  btwnoutside  36360  outsideoftr  36364  lineunray  36382  lineelsb2  36383  cnres2  38137  heibor  38195  lsmcv2  39528  lcvat  39529  lcvexchlem4  39536  lcvexchlem5  39537  lfladd  39565  lflsub  39566  lflmul  39567  lshpkrlem4  39612  latm4  39732  omlmod1i2N  39759  cvlatexch3  39837  cvlsupr7  39847  hlatj4  39873  hlrelat3  39911  cvrval3  39912  atcvrj1  39930  atlelt  39937  2atlt  39938  2atjm  39944  3noncolr2  39948  athgt  39955  3dimlem2  39958  3dimlem4  39963  3dimlem4OLDN  39964  3dim3  39968  1cvratex  39972  ps-1  39976  ps-2  39977  hlatexch3N  39979  llnle  40017  atcvrlln2  40018  atcvrlln  40019  lplni2  40036  lplnle  40039  lplnnle2at  40040  llncvrlpln2  40056  lplnexllnN  40063  2llnmeqat  40070  lvolnle3at  40081  4atlem0ae  40093  lplncvrlvol2  40114  lnjatN  40279  lncvrat  40281  cdlemblem  40292  elpaddri  40301  paddasslem2  40320  paddasslem16  40334  padd4N  40339  hlmod1i  40355  dalawlem2  40371  pclfinN  40399  pexmidlem4N  40472  pl42lem1N  40478  lhp2lt  40500  lhpexle1  40507  lhpexle2lem  40508  lhpj1  40521  lhpmcvr5N  40526  lhp2at0  40531  lhp2atnle  40532  lhp2at0nle  40534  lhple  40541  lhpat  40542  lhpat4N  40543  4atexlempnq  40554  4atexlem7  40574  4atex  40575  ltrn11  40625  ltrnle  40628  ltrnm  40630  ltrnj  40631  ltrncvr  40632  ltrnel  40638  ltrncnvel  40641  ltrncnv  40645  trlval2  40662  trlcnv  40664  trljat1  40665  trljat2  40666  trlat  40668  trl0  40669  trlnidat  40672  trlnid  40678  cdlemc1  40690  cdlemc2  40691  cdlemc5  40694  cdlemd2  40698  cdlemd7  40703  cdlemd8  40704  cdlemd9  40705  cdleme0e  40716  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme5  40739  cdleme10  40753  cdleme11a  40759  cdleme11c  40760  cdleme11h  40765  cdleme11j  40766  cdleme0nex  40789  cdleme18a  40790  cdleme18b  40791  cdleme22gb  40793  cdleme20zN  40800  cdleme20c  40810  cdleme20k  40818  cdleme21a  40824  cdleme21b  40825  cdleme21c  40826  cdleme21h  40833  cdleme22b  40840  cdleme22d  40842  cdleme22f  40845  cdleme25a  40852  cdleme25c  40854  cdleme25dN  40855  cdleme26ee  40859  cdleme30a  40877  cdlemefr29bpre0N  40905  cdlemefr29clN  40906  cdlemefr32fvaN  40908  cdlemefr32fva1  40909  cdlemefs29bpre0N  40915  cdlemefs29bpre1N  40916  cdlemefs29cpre1N  40917  cdlemefs29clN  40918  cdleme43fsv1snlem  40919  cdlemefs32fvaN  40921  cdlemefs32fva1  40922  cdlemefs31fv1  40923  cdleme36a  40959  cdleme39a  40964  cdleme42a  40970  cdleme42c  40971  cdleme17d3  40995  cdleme48fv  40998  cdleme48bw  41001  cdleme48b  41002  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemeg46gfv  41029  cdleme48d  41034  cdleme50trn2a  41049  cdleme50trn2  41050  cdleme50ltrn  41056  cdlemf1  41060  cdlemf  41062  trlord  41068  cdlemg2dN  41089  cdlemg2fvlem  41093  cdlemg2l  41102  cdlemg7fvbwN  41106  cdlemg7aN  41124  cdlemg10bALTN  41135  cdlemg10c  41138  cdlemg17a  41160  cdlemg17dALTN  41163  cdlemg31b0a  41194  cdlemg31a  41196  cdlemg31b  41197  cdlemg34  41211  cdlemg36  41213  ltrnco  41218  trlcoabs2N  41221  trlcolem  41225  cdlemg48  41236  tgrpov  41247  tendoco2  41267  tendoplco2  41278  cdlemh1  41314  cdlemi1  41317  cdlemi2  41318  cdlemj3  41322  tendoid0  41324  cdlemk1  41330  cdlemk2  41331  cdlemk4  41333  cdlemk8  41337  cdlemk9  41338  cdlemk9bN  41339  cdlemk10  41342  cdlemk26b-3  41404  cdlemk26-3  41405  cdlemk28-3  41407  cdlemk37  41413  cdlemk39  41415  cdlemkfid1N  41420  cdlemkid1  41421  cdlemky  41425  cdlemkyu  41426  cdlemk19ylem  41429  cdlemk19xlem  41441  cdlemk11t  41445  cdlemk51  41452  cdlemkyyN  41461  cdleml6  41480  cdleml7  41481  cdleml8  41482  cdleml9  41483  erngdvlem4  41490  erngdvlem4-rN  41498  tendospcanN  41522  dia11N  41547  cdlemm10N  41617  dib11N  41659  dicvaddcl  41689  dicvscacl  41690  cdlemn6  41701  dihvalcq2  41746  dihopelvalcpre  41747  dihord6b  41759  dihord5apre  41761  dihmeetlem1N  41789  dihmeetlem2N  41798  dihglbcpreN  41799  dihjatc1  41810  dihmeetlem20N  41825  dih1dimatlem0  41827  dihatlat  41833  dihglblem6  41839  dochexmidlem4  41962  mapdpglem32  42204  mapdh8ad  42278  mapdh9aOLDN  42289  hdmap11lem2  42341  hdmap14lem6  42372  frlmfzowrdb  43001  flt4lem5  43107  mzpsubst  43204  pellex  43287  pellfundex  43338  pellfund14gap  43339  qirropth  43360  rmxypos  43399  congmul  43419  congsub  43422  mzpcong  43424  coprmdvdsb  43437  jm2.15nn0  43455  jm2.16nn0  43456  rpnnen3lem  43483  idomsubgmo  43645  relexp01min  44164  mullimc  46068  islptre  46071  limccog  46072  mullimcf  46075  addlimc  46098  0ellimcdiv  46099  limsupre3lem  46182  stoweidlem57  46507  fourierdlem48  46604  fourierdlem80  46636  fourierdlem113  46669  ovncvrrp  47014  opnvonmbllem2  47083  ovolval5lem3  47104  ovnovollem3  47108  grlimedgclnbgr  48493  itsclc0lem1  49254  itsclc0lem2  49255  itschlc0yqe  49258  itscnhlc0xyqsol  49263  itschlc0xyqsol1  49264  swapffunc  49779  fucofunc  49856  fucoppc  49907