Theorem simp3r 1203

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp13r  1290  simp23r  1296  simp33r  1302  f1oiso2  7294  tfisi  7797  tfrlem5  8307  omeulem1  8505  omeulem2  8506  elfiun  9323  isfin2-2  10219  addlid  11305  mulcan  11763  mulcan2  11764  divass  11803  divdir  11810  div11OLD  11814  ltdiv1  11995  ltmuldiv  12004  lediv2  12021  xaddass2  13153  xlt2add  13163  expaddz  14017  expmulz  14019  resqrex  15161  resqrtcl  15164  o1add  15525  o1mul  15526  o1sub  15527  dvdsgcd  16459  rpexp12i  16639  pythagtriplem4  16735  pythagtriplem11  16741  pythagtriplem13  16743  pcpremul  16759  pceu  16762  pcqmul  16769  pcqdiv  16773  f1ocpbllem  17432  funcoppc  17786  funcres  17807  catcisolem  18021  1stfcl  18107  2ndfcl  18108  prfcl  18113  evlfcl  18132  curf1cl  18138  curfcl  18142  hofcl  18169  latjlej12  18365  latmlem12  18381  latj4  18399  latj4rot  18400  symgsssg  19383  symgfisg  19384  odcong  19465  cmn4  19717  ablsub4  19726  abladdsub4  19727  lsm4  19776  abvdom  20749  abvtrivd  20751  orngmul  20784  lspsolvlem  21083  lbsextlem2  21100  lidlsubcl  21165  frlmbas3  21717  matinvgcell  22353  matmulcell  22363  ma1repveval  22489  mdetunilem3  22532  mdetuni0  22539  mdetmul  22541  hausflimlem  23897  psmetlecl  24233  xmetlecl  24264  prdsxmetlem  24286  xblcntrps  24328  xblcntr  24329  bndth  24887  cph2ass  25143  iscau3  25208  dvres2  25843  coemullem  26185  vieta1  26250  aalioulem4  26273  cxpcn3lem  26687  angcan  26742  divsqrtsumlem  26920  dchrmusumlema  27434  dchrvmasumlema  27441  dchrisum0lema  27455  logdivsum  27474  padicabv  27571  cofcut1  27867  cofcut2  27869  divsmulw  28135  precsexlem8  28155  precsexlem9  28156  ax5seglem3  28913  ax5seglem6  28916  axpasch  28923  axeuclid  28945  axcontlem4  28949  axcontlem8  28953  trlsonistrl  29689  pthonispth  29728  spthonisspth  29732  wspthneq1eq2  29842  frgr2wwlkeqm  30315  adjlnop  32070  xreceu  32911  rhmdvd  33298  measvunilem  34248  measvuni  34250  bnj1128  35025  umgr2cycl  35208  satfv1fvfmla1  35490  cgrcomim  36056  cgrcoml  36063  cgrcomr  36064  cgrdegen  36071  segconeu  36078  btwnintr  36086  btwnexch3  36087  btwnouttr2  36089  btwnouttr  36091  btwnexch  36092  ifscgr  36111  lineext  36143  linecgr  36148  lineid  36150  idinside  36151  btwnconn1lem3  36156  btwnconn1lem4  36157  btwnconn1lem14  36167  btwnconn2  36169  btwnconn3  36170  midofsegid  36171  btwnoutside  36192  outsideoftr  36196  lineunray  36214  lineelsb2  36215  itg2addnclem  37734  cnres2  37826  heibor  37884  lsmcv2  39151  lcvat  39152  lcvexchlem4  39159  lcvexchlem5  39160  lfladd  39188  lflsub  39189  lflmul  39190  lshpkrlem4  39235  latm4  39355  omlmod1i2N  39382  cvlsupr7  39470  cvlsupr8  39471  hlatj4  39496  hlrelat3  39534  cvrval3  39535  atcvrj1  39553  atlelt  39560  2atlt  39561  2atjm  39567  3noncolr2  39571  athgt  39578  3dimlem2  39581  3dimlem4OLDN  39587  1cvratex  39595  ps-1  39599  ps-2  39600  hlatexch3N  39602  llnle  39640  atcvrlln2  39641  atcvrlln  39642  lplni2  39659  lplnle  39662  lplnnle2at  39663  lplnnlelln  39665  llncvrlpln2  39679  2llnmeqat  39693  lvolnle3at  39704  lvolnlelln  39706  4atlem0ae  39716  lneq2at  39900  lnjatN  39902  lncvrat  39904  2lnat  39906  elpaddri  39924  paddasslem2  39943  padd4N  39962  hlmod1i  39978  llnexchb2  39991  dalawlem2  39994  pclfinN  40022  pexmidlem4N  40095  pl42lem1N  40101  lhp2lt  40123  lhpexle1  40130  lhpexle2lem  40131  lhpj1  40144  lhpmcvr5N  40149  lhp2at0  40154  lhp2at0nle  40157  lhple  40164  lhpat  40165  lhpat4N  40166  4atexlemnslpq  40178  4atexlem7  40197  ltrn11  40248  ltrnle  40251  ltrnm  40253  ltrnj  40254  ltrncvr  40255  ltrnel  40261  ltrncnvel  40264  ltrncnv  40268  trlat  40291  trl0  40292  trlnidat  40295  trlnid  40301  ltrnatlw  40305  trlne  40307  trlval4  40310  cdlemc5  40317  cdlemd2  40321  cdlemd7  40326  cdlemd8  40327  cdlemd9  40328  cdleme0c  40335  cdleme0e  40339  cdleme0fN  40340  cdleme3g  40356  cdleme3h  40357  cdleme5  40362  cdleme11c  40383  cdleme11h  40388  cdleme11j  40389  cdleme11k  40390  cdleme0nex  40412  cdleme18a  40413  cdleme22gb  40416  cdleme20zN  40423  cdleme20c  40433  cdleme20k  40441  cdleme21a  40447  cdleme21b  40448  cdleme21c  40449  cdleme21ct  40451  cdleme21h  40456  cdleme22d  40465  cdleme22f  40468  cdleme26ee  40482  cdleme30a  40500  cdlemefs45eN  40553  cdleme36a  40582  cdleme36m  40583  cdleme39a  40587  cdleme42b  40600  cdleme43dN  40614  cdlemeg47rv2  40632  cdlemeg46sfg  40642  cdlemeg46rjgN  40644  cdlemeg46rgv  40650  cdlemeg46req  40651  cdlemeg46gfv  40652  cdleme48d  40657  cdleme50ltrn  40679  cdlemf1  40683  cdlemf  40685  cdlemg2dN  40712  cdlemg2fvlem  40716  cdlemg2l  40725  cdlemg7fvbwN  40729  cdlemg7aN  40747  cdlemg10c  40761  cdlemg17a  40783  cdlemg17dALTN  40786  cdlemg18a  40800  cdlemg18b  40801  cdlemg31b0a  40817  cdlemg31a  40819  cdlemg31b  40820  ltrnco  40841  cdlemg48  40859  tgrpov  40870  tendoco2  40890  tendoplco2  40901  cdlemh1  40937  cdlemk1  40953  cdlemk26b-3  41027  cdlemk27-3  41029  cdlemk28-3  41030  cdlemk34  41032  cdlemkfid1N  41043  cdlemkid3N  41055  cdlemkid4  41056  cdlemk35s-id  41060  cdlemk39s-id  41062  cdlemk51  41075  tendospcanN  41145  cdlemm10N  41240  dicvaddcl  41312  dicvscacl  41313  cdlemn6  41324  dihvalcq2  41369  dihord6b  41382  dihord5apre  41384  dihglbcpreN  41422  dihjatc1  41433  dihmeetlem20N  41448  dih1dimatlem0  41450  dihglblem6  41462  dochexmidlem4  41585  mapdpglem32  41827  mapdh8ad  41901  mapdh9aOLDN  41912  hdmap11lem2  41964  hdmap14lem6  41995  frlmfzowrdb  42625  mzpmfp  42867  mzpsubst  42868  pellex  42955  pellfundex  43006  pellfund14gap  43007  qirropth  43028  rmxypos  43067  congmul  43087  congsub  43090  mzpcong  43092  coprmdvdsb  43105  jm2.15nn0  43123  jm2.16nn0  43124  rpnnen3lem  43151  idomsubgmo  43313  relexp01min  43833  mullimc  45743  islptre  45746  mullimcf  45750  addlimc  45773  0ellimcdiv  45774  limsupre3lem  45857  limsupre3uzlem  45860  fourierdlem48  46279  fourierdlem80  46311  opnvonmbllem2  46758  ovolval5lem3  46779  ovnovollem3  46783  difltmodne  47469  isubgr3stgrlem1  48093  grlimedgclnbgr  48122  mapprop  48473  lincfsuppcl  48541  lindslinindimp2lem3  48588  itsclc0lem1  48884  itsclc0lem2  48885  itschlc0yqe  48888  itsclc0xyqsolr  48897  swapffunc  49410  fucofunc  49487  fucoppc  49538