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  7289  tfisi  7792  tfrlem5  8302  omeulem1  8500  omeulem2  8501  elfiun  9320  isfin2-2  10213  addlid  11299  mulcan  11757  mulcan2  11758  divass  11797  divdir  11804  div11OLD  11808  ltdiv1  11989  ltmuldiv  11998  lediv2  12015  xaddass2  13152  xlt2add  13162  expaddz  14013  expmulz  14015  resqrex  15157  resqrtcl  15160  o1add  15521  o1mul  15522  o1sub  15523  dvdsgcd  16455  rpexp12i  16635  pythagtriplem4  16731  pythagtriplem11  16737  pythagtriplem13  16739  pcpremul  16755  pceu  16758  pcqmul  16765  pcqdiv  16769  f1ocpbllem  17428  funcoppc  17782  funcres  17803  catcisolem  18017  1stfcl  18103  2ndfcl  18104  prfcl  18109  evlfcl  18128  curf1cl  18134  curfcl  18138  hofcl  18165  latjlej12  18361  latmlem12  18377  latj4  18395  latj4rot  18396  symgsssg  19346  symgfisg  19347  odcong  19428  cmn4  19680  ablsub4  19689  abladdsub4  19690  lsm4  19739  abvdom  20715  abvtrivd  20717  orngmul  20750  lspsolvlem  21049  lbsextlem2  21066  lidlsubcl  21131  frlmbas3  21683  matinvgcell  22320  matmulcell  22330  ma1repveval  22456  mdetunilem3  22499  mdetuni0  22506  mdetmul  22508  hausflimlem  23864  psmetlecl  24201  xmetlecl  24232  prdsxmetlem  24254  xblcntrps  24296  xblcntr  24297  bndth  24855  cph2ass  25111  iscau3  25176  dvres2  25811  coemullem  26153  vieta1  26218  aalioulem4  26241  cxpcn3lem  26655  angcan  26710  divsqrtsumlem  26888  dchrmusumlema  27402  dchrvmasumlema  27409  dchrisum0lema  27423  logdivsum  27442  padicabv  27539  cofcut1  27833  cofcut2  27835  divsmulw  28101  precsexlem8  28121  precsexlem9  28122  ax5seglem3  28876  ax5seglem6  28879  axpasch  28886  axeuclid  28908  axcontlem4  28912  axcontlem8  28916  trlsonistrl  29652  pthonispth  29691  spthonisspth  29695  wspthneq1eq2  29805  frgr2wwlkeqm  30275  adjlnop  32030  xreceu  32863  rhmdvd  33263  measvunilem  34185  measvuni  34187  bnj1128  34963  umgr2cycl  35124  satfv1fvfmla1  35406  cgrcomim  35973  cgrcoml  35980  cgrcomr  35981  cgrdegen  35988  segconeu  35995  btwnintr  36003  btwnexch3  36004  btwnouttr2  36006  btwnouttr  36008  btwnexch  36009  ifscgr  36028  lineext  36060  linecgr  36065  lineid  36067  idinside  36068  btwnconn1lem3  36073  btwnconn1lem4  36074  btwnconn1lem14  36084  btwnconn2  36086  btwnconn3  36087  midofsegid  36088  btwnoutside  36109  outsideoftr  36113  lineunray  36131  lineelsb2  36132  itg2addnclem  37661  cnres2  37753  heibor  37811  lsmcv2  39018  lcvat  39019  lcvexchlem4  39026  lcvexchlem5  39027  lfladd  39055  lflsub  39056  lflmul  39057  lshpkrlem4  39102  latm4  39222  omlmod1i2N  39249  cvlsupr7  39337  cvlsupr8  39338  hlatj4  39363  hlrelat3  39401  cvrval3  39402  atcvrj1  39420  atlelt  39427  2atlt  39428  2atjm  39434  3noncolr2  39438  athgt  39445  3dimlem2  39448  3dimlem4OLDN  39454  1cvratex  39462  ps-1  39466  ps-2  39467  hlatexch3N  39469  llnle  39507  atcvrlln2  39508  atcvrlln  39509  lplni2  39526  lplnle  39529  lplnnle2at  39530  lplnnlelln  39532  llncvrlpln2  39546  2llnmeqat  39560  lvolnle3at  39571  lvolnlelln  39573  4atlem0ae  39583  lneq2at  39767  lnjatN  39769  lncvrat  39771  2lnat  39773  elpaddri  39791  paddasslem2  39810  padd4N  39829  hlmod1i  39845  llnexchb2  39858  dalawlem2  39861  pclfinN  39889  pexmidlem4N  39962  pl42lem1N  39968  lhp2lt  39990  lhpexle1  39997  lhpexle2lem  39998  lhpj1  40011  lhpmcvr5N  40016  lhp2at0  40021  lhp2at0nle  40024  lhple  40031  lhpat  40032  lhpat4N  40033  4atexlemnslpq  40045  4atexlem7  40064  ltrn11  40115  ltrnle  40118  ltrnm  40120  ltrnj  40121  ltrncvr  40122  ltrnel  40128  ltrncnvel  40131  ltrncnv  40135  trlat  40158  trl0  40159  trlnidat  40162  trlnid  40168  ltrnatlw  40172  trlne  40174  trlval4  40177  cdlemc5  40184  cdlemd2  40188  cdlemd7  40193  cdlemd8  40194  cdlemd9  40195  cdleme0c  40202  cdleme0e  40206  cdleme0fN  40207  cdleme3g  40223  cdleme3h  40224  cdleme5  40229  cdleme11c  40250  cdleme11h  40255  cdleme11j  40256  cdleme11k  40257  cdleme0nex  40279  cdleme18a  40280  cdleme22gb  40283  cdleme20zN  40290  cdleme20c  40300  cdleme20k  40308  cdleme21a  40314  cdleme21b  40315  cdleme21c  40316  cdleme21ct  40318  cdleme21h  40323  cdleme22d  40332  cdleme22f  40335  cdleme26ee  40349  cdleme30a  40367  cdlemefs45eN  40420  cdleme36a  40449  cdleme36m  40450  cdleme39a  40454  cdleme42b  40467  cdleme43dN  40481  cdlemeg47rv2  40499  cdlemeg46sfg  40509  cdlemeg46rjgN  40511  cdlemeg46rgv  40517  cdlemeg46req  40518  cdlemeg46gfv  40519  cdleme48d  40524  cdleme50ltrn  40546  cdlemf1  40550  cdlemf  40552  cdlemg2dN  40579  cdlemg2fvlem  40583  cdlemg2l  40592  cdlemg7fvbwN  40596  cdlemg7aN  40614  cdlemg10c  40628  cdlemg17a  40650  cdlemg17dALTN  40653  cdlemg18a  40667  cdlemg18b  40668  cdlemg31b0a  40684  cdlemg31a  40686  cdlemg31b  40687  ltrnco  40708  cdlemg48  40726  tgrpov  40737  tendoco2  40757  tendoplco2  40768  cdlemh1  40804  cdlemk1  40820  cdlemk26b-3  40894  cdlemk27-3  40896  cdlemk28-3  40897  cdlemk34  40899  cdlemkfid1N  40910  cdlemkid3N  40922  cdlemkid4  40923  cdlemk35s-id  40927  cdlemk39s-id  40929  cdlemk51  40942  tendospcanN  41012  cdlemm10N  41107  dicvaddcl  41179  dicvscacl  41180  cdlemn6  41191  dihvalcq2  41236  dihord6b  41249  dihord5apre  41251  dihglbcpreN  41289  dihjatc1  41300  dihmeetlem20N  41315  dih1dimatlem0  41317  dihglblem6  41329  dochexmidlem4  41452  mapdpglem32  41694  mapdh8ad  41768  mapdh9aOLDN  41779  hdmap11lem2  41831  hdmap14lem6  41862  frlmfzowrdb  42487  mzpmfp  42730  mzpsubst  42731  pellex  42818  pellfundex  42869  pellfund14gap  42870  qirropth  42891  rmxypos  42930  congmul  42950  congsub  42953  mzpcong  42955  coprmdvdsb  42968  jm2.15nn0  42986  jm2.16nn0  42987  rpnnen3lem  43014  idomsubgmo  43176  relexp01min  43696  mullimc  45607  islptre  45610  mullimcf  45614  addlimc  45639  0ellimcdiv  45640  limsupre3lem  45723  limsupre3uzlem  45726  fourierdlem48  46145  fourierdlem80  46177  opnvonmbllem2  46624  ovolval5lem3  46645  ovnovollem3  46649  difltmodne  47336  isubgr3stgrlem1  47960  grlimedgclnbgr  47989  mapprop  48340  lincfsuppcl  48408  lindslinindimp2lem3  48455  itsclc0lem1  48751  itsclc0lem2  48752  itschlc0yqe  48755  itsclc0xyqsolr  48764  swapffunc  49277  fucofunc  49354  fucoppc  49405