Theorem simp3r 1221

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

Assertion

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

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 490	. 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:  simp13r  1308  simp23r  1314  simp33r  1320  f1oiso2  7357  tfisi  7859  tfrlem5  8372  omeulem1  8573  omeulem2  8574  elfiun  9404  isfin2-2  10325  addlid  11421  mulcan  11879  mulcan2  11880  divass  11918  divdir  11925  ltdiv1  12107  ltmuldiv  12116  lediv2  12133  xaddass2  13306  xlt2add  13316  expaddz  14174  expmulz  14176  resqrex  15341  resqrtcl  15344  o1add  15705  o1mul  15706  o1sub  15707  dvdsgcd  16640  rpexp12i  16821  pythagtriplem4  16917  pythagtriplem11  16923  pythagtriplem13  16925  pcpremul  16941  pceu  16944  pcqmul  16951  pcqdiv  16955  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  odcong  19682  cmn4  19934  ablsub4  19943  abladdsub4  19944  lsm4  19993  abvdom  21002  abvtrivd  21004  orngmul  21037  lspsolvlem  21335  lbsextlem2  21352  lidlsubcl  21418  frlmbas3  21995  matinvgcell  22663  matmulcell  22673  ma1repveval  22799  mdetunilem3  22842  mdetuni0  22849  mdetmul  22851  hausflimlem  24211  psmetlecl  24547  xmetlecl  24578  prdsxmetlem  24600  xblcntrps  24642  xblcntr  24643  bndth  25192  cph2ass  25447  iscau3  25512  dvres2  26146  coemullem  26483  vieta1  26551  aalioulem4  26578  cxpcn3lem  26992  angcan  27047  divsqrtsumlem  27224  dchrmusumlema  27737  dchrvmasumlema  27744  dchrisum0lema  27758  logdivsum  27777  padicabv  27874  cofcut1  28193  cofcut2  28195  divmulsw  28466  precsexlem8  28487  precsexlem9  28488  bdayfinbndlem1  28740  ax5seglem3  29396  ax5seglem6  29399  axpasch  29406  axeuclid  29428  axcontlem4  29432  axcontlem8  29436  trlsonistrl  30178  pthonispth  30219  spthonisspth  30223  wspthneq1eq2  30336  umgr2cycllem  30633  umgr2cycl  30634  frgr2wwlkeqm  30819  adjlnop  32575  xreceu  33375  rhmdvd  33772  measvunilem  34731  measvuni  34733  bnj1128  35507  satfv1fvfmla1  36010  cgrcomim  36577  cgrcoml  36584  cgrcomr  36585  cgrdegen  36592  segconeu  36599  btwnintr  36607  btwnexch3  36608  btwnouttr2  36610  btwnouttr  36612  btwnexch  36613  ifscgr  36632  lineext  36664  linecgr  36669  lineid  36671  idinside  36672  btwnconn1lem3  36677  btwnconn1lem4  36678  btwnconn1lem14  36688  btwnconn2  36690  btwnconn3  36691  midofsegid  36692  btwnoutside  36713  outsideoftr  36717  lineunray  36735  lineelsb2  36736  itg2addnclem  38428  cnres2  38521  heibor  38579  lsmcv2  39910  lcvat  39911  lcvexchlem4  39918  lcvexchlem5  39919  lfladd  39947  lflsub  39948  lflmul  39949  lshpkrlem4  39994  latm4  40114  omlmod1i2N  40141  cvlsupr7  40229  cvlsupr8  40230  hlatj4  40255  hlrelat3  40293  cvrval3  40294  atcvrj1  40312  atlelt  40319  2atlt  40320  2atjm  40326  3noncolr2  40330  athgt  40337  3dimlem2  40340  3dimlem4OLDN  40346  1cvratex  40354  ps-1  40358  ps-2  40359  hlatexch3N  40361  llnle  40399  atcvrlln2  40400  atcvrlln  40401  lplni2  40418  lplnle  40421  lplnnle2at  40422  lplnnlelln  40424  llncvrlpln2  40438  2llnmeqat  40452  lvolnle3at  40463  lvolnlelln  40465  4atlem0ae  40475  lneq2at  40659  lnjatN  40661  lncvrat  40663  2lnat  40665  elpaddri  40683  paddasslem2  40702  padd4N  40721  hlmod1i  40737  llnexchb2  40750  dalawlem2  40753  pclfinN  40781  pexmidlem4N  40854  pl42lem1N  40860  lhp2lt  40882  lhpexle1  40889  lhpexle2lem  40890  lhpj1  40903  lhpmcvr5N  40908  lhp2at0  40913  lhp2at0nle  40916  lhple  40923  lhpat  40924  lhpat4N  40925  4atexlemnslpq  40937  4atexlem7  40956  ltrn11  41007  ltrnle  41010  ltrnm  41012  ltrnj  41013  ltrncvr  41014  ltrnel  41020  ltrncnvel  41023  ltrncnv  41027  trlat  41050  trl0  41051  trlnidat  41054  trlnid  41060  ltrnatlw  41064  trlne  41066  trlval4  41069  cdlemc5  41076  cdlemd2  41080  cdlemd7  41085  cdlemd8  41086  cdlemd9  41087  cdleme0c  41094  cdleme0e  41098  cdleme0fN  41099  cdleme3g  41115  cdleme3h  41116  cdleme5  41121  cdleme11c  41142  cdleme11h  41147  cdleme11j  41148  cdleme11k  41149  cdleme0nex  41171  cdleme18a  41172  cdleme22gb  41175  cdleme20zN  41182  cdleme20c  41192  cdleme20k  41200  cdleme21a  41206  cdleme21b  41207  cdleme21c  41208  cdleme21ct  41210  cdleme21h  41215  cdleme22d  41224  cdleme22f  41227  cdleme26ee  41241  cdleme30a  41259  cdlemefs45eN  41312  cdleme36a  41341  cdleme36m  41342  cdleme39a  41346  cdleme42b  41359  cdleme43dN  41373  cdlemeg47rv2  41391  cdlemeg46sfg  41401  cdlemeg46rjgN  41403  cdlemeg46rgv  41409  cdlemeg46req  41410  cdlemeg46gfv  41411  cdleme48d  41416  cdleme50ltrn  41438  cdlemf1  41442  cdlemf  41444  cdlemg2dN  41471  cdlemg2fvlem  41475  cdlemg2l  41484  cdlemg7fvbwN  41488  cdlemg7aN  41506  cdlemg10c  41520  cdlemg17a  41542  cdlemg17dALTN  41545  cdlemg18a  41559  cdlemg18b  41560  cdlemg31b0a  41576  cdlemg31a  41578  cdlemg31b  41579  ltrnco  41600  cdlemg48  41618  tgrpov  41629  tendoco2  41649  tendoplco2  41660  cdlemh1  41696  cdlemk1  41712  cdlemk26b-3  41786  cdlemk27-3  41788  cdlemk28-3  41789  cdlemk34  41791  cdlemkfid1N  41802  cdlemkid3N  41814  cdlemkid4  41815  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk51  41834  tendospcanN  41904  cdlemm10N  41999  dicvaddcl  42071  dicvscacl  42072  cdlemn6  42083  dihvalcq2  42128  dihord6b  42141  dihord5apre  42143  dihglbcpreN  42181  dihjatc1  42192  dihmeetlem20N  42207  dih1dimatlem0  42209  dihglblem6  42221  dochexmidlem4  42344  mapdpglem32  42586  mapdh8ad  42660  mapdh9aOLDN  42671  hdmap11lem2  42723  hdmap14lem6  42754  frlmfzowrdb  43400  mzpmfp  43600  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  mullimcf  46461  addlimc  46484  0ellimcdiv  46485  limsupre3lem  46568  limsupre3uzlem  46571  fourierdlem48  46990  fourierdlem80  47022  opnvonmbllem2  47469  ovolval5lem3  47490  ovnovollem3  47494  difltmodne  48244  isubgr3stgrlem1  48890  grlimedgclnbgr  48919  mapprop  49284  lincfsuppcl  49351  lindslinindimp2lem3  49398  itsclc0lem1  49694  itsclc0lem2  49695  itschlc0yqe  49698  itsclc0xyqsolr  49707  swapffunc  50216  fucofunc  50293  fucoppc  50344