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  7361  tfisi  7864  tfrlem5  8375  omeulem1  8576  omeulem2  8577  elfiun  9400  isfin2-2  10321  addlid  11411  mulcan  11869  mulcan2  11870  divass  11908  divdir  11915  ltdiv1  12097  ltmuldiv  12106  lediv2  12123  xaddass2  13294  xlt2add  13304  expaddz  14162  expmulz  14164  resqrex  15327  resqrtcl  15330  o1add  15691  o1mul  15692  o1sub  15693  dvdsgcd  16627  rpexp12i  16808  pythagtriplem4  16904  pythagtriplem11  16910  pythagtriplem13  16912  pcpremul  16928  pceu  16931  pcqmul  16938  pcqdiv  16942  f1ocpbllem  17603  funcoppc  17957  funcres  17978  catcisolem  18192  1stfcl  18278  2ndfcl  18279  prfcl  18284  evlfcl  18303  curf1cl  18309  curfcl  18313  hofcl  18340  latjlej12  18536  latmlem12  18552  latj4  18570  latj4rot  18571  symgsssg  19568  symgfisg  19569  odcong  19650  cmn4  19902  ablsub4  19911  abladdsub4  19912  lsm4  19961  abvdom  20970  abvtrivd  20972  orngmul  21005  lspsolvlem  21303  lbsextlem2  21320  lidlsubcl  21386  frlmbas3  21963  matinvgcell  22629  matmulcell  22639  ma1repveval  22765  mdetunilem3  22808  mdetuni0  22815  mdetmul  22817  hausflimlem  24173  psmetlecl  24509  xmetlecl  24540  prdsxmetlem  24562  xblcntrps  24604  xblcntr  24605  bndth  25154  cph2ass  25409  iscau3  25474  dvres2  26108  coemullem  26444  vieta1  26510  aalioulem4  26535  cxpcn3lem  26949  angcan  27004  divsqrtsumlem  27181  dchrmusumlema  27694  dchrvmasumlema  27701  dchrisum0lema  27715  logdivsum  27734  padicabv  27831  cofcut1  28150  cofcut2  28152  divmulsw  28423  precsexlem8  28444  precsexlem9  28445  bdayfinbndlem1  28697  ax5seglem3  29318  ax5seglem6  29321  axpasch  29328  axeuclid  29350  axcontlem4  29354  axcontlem8  29358  trlsonistrl  30093  pthonispth  30132  spthonisspth  30136  wspthneq1eq2  30246  frgr2wwlkeqm  30719  adjlnop  32475  xreceu  33278  rhmdvd  33675  measvunilem  34634  measvuni  34636  bnj1128  35410  umgr2cycl  35654  satfv1fvfmla1  35936  cgrcomim  36502  cgrcoml  36509  cgrcomr  36510  cgrdegen  36517  segconeu  36524  btwnintr  36532  btwnexch3  36533  btwnouttr2  36535  btwnouttr  36537  btwnexch  36538  ifscgr  36557  lineext  36589  linecgr  36594  lineid  36596  idinside  36597  btwnconn1lem3  36602  btwnconn1lem4  36603  btwnconn1lem14  36613  btwnconn2  36615  btwnconn3  36616  midofsegid  36617  btwnoutside  36638  outsideoftr  36642  lineunray  36660  lineelsb2  36661  itg2addnclem  38363  cnres2  38455  heibor  38513  lsmcv2  39844  lcvat  39845  lcvexchlem4  39852  lcvexchlem5  39853  lfladd  39881  lflsub  39882  lflmul  39883  lshpkrlem4  39928  latm4  40048  omlmod1i2N  40075  cvlsupr7  40163  cvlsupr8  40164  hlatj4  40189  hlrelat3  40227  cvrval3  40228  atcvrj1  40246  atlelt  40253  2atlt  40254  2atjm  40260  3noncolr2  40264  athgt  40271  3dimlem2  40274  3dimlem4OLDN  40280  1cvratex  40288  ps-1  40292  ps-2  40293  hlatexch3N  40295  llnle  40333  atcvrlln2  40334  atcvrlln  40335  lplni2  40352  lplnle  40355  lplnnle2at  40356  lplnnlelln  40358  llncvrlpln2  40372  2llnmeqat  40386  lvolnle3at  40397  lvolnlelln  40399  4atlem0ae  40409  lneq2at  40593  lnjatN  40595  lncvrat  40597  2lnat  40599  elpaddri  40617  paddasslem2  40636  padd4N  40655  hlmod1i  40671  llnexchb2  40684  dalawlem2  40687  pclfinN  40715  pexmidlem4N  40788  pl42lem1N  40794  lhp2lt  40816  lhpexle1  40823  lhpexle2lem  40824  lhpj1  40837  lhpmcvr5N  40842  lhp2at0  40847  lhp2at0nle  40850  lhple  40857  lhpat  40858  lhpat4N  40859  4atexlemnslpq  40871  4atexlem7  40890  ltrn11  40941  ltrnle  40944  ltrnm  40946  ltrnj  40947  ltrncvr  40948  ltrnel  40954  ltrncnvel  40957  ltrncnv  40961  trlat  40984  trl0  40985  trlnidat  40988  trlnid  40994  ltrnatlw  40998  trlne  41000  trlval4  41003  cdlemc5  41010  cdlemd2  41014  cdlemd7  41019  cdlemd8  41020  cdlemd9  41021  cdleme0c  41028  cdleme0e  41032  cdleme0fN  41033  cdleme3g  41049  cdleme3h  41050  cdleme5  41055  cdleme11c  41076  cdleme11h  41081  cdleme11j  41082  cdleme11k  41083  cdleme0nex  41105  cdleme18a  41106  cdleme22gb  41109  cdleme20zN  41116  cdleme20c  41126  cdleme20k  41134  cdleme21a  41140  cdleme21b  41141  cdleme21c  41142  cdleme21ct  41144  cdleme21h  41149  cdleme22d  41158  cdleme22f  41161  cdleme26ee  41175  cdleme30a  41193  cdlemefs45eN  41246  cdleme36a  41275  cdleme36m  41276  cdleme39a  41280  cdleme42b  41293  cdleme43dN  41307  cdlemeg47rv2  41325  cdlemeg46sfg  41335  cdlemeg46rjgN  41337  cdlemeg46rgv  41343  cdlemeg46req  41344  cdlemeg46gfv  41345  cdleme48d  41350  cdleme50ltrn  41372  cdlemf1  41376  cdlemf  41378  cdlemg2dN  41405  cdlemg2fvlem  41409  cdlemg2l  41418  cdlemg7fvbwN  41422  cdlemg7aN  41440  cdlemg10c  41454  cdlemg17a  41476  cdlemg17dALTN  41479  cdlemg18a  41493  cdlemg18b  41494  cdlemg31b0a  41510  cdlemg31a  41512  cdlemg31b  41513  ltrnco  41534  cdlemg48  41552  tgrpov  41563  tendoco2  41583  tendoplco2  41594  cdlemh1  41630  cdlemk1  41646  cdlemk26b-3  41720  cdlemk27-3  41722  cdlemk28-3  41723  cdlemk34  41725  cdlemkfid1N  41736  cdlemkid3N  41748  cdlemkid4  41749  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk51  41768  tendospcanN  41838  cdlemm10N  41933  dicvaddcl  42005  dicvscacl  42006  cdlemn6  42017  dihvalcq2  42062  dihord6b  42075  dihord5apre  42077  dihglbcpreN  42115  dihjatc1  42126  dihmeetlem20N  42141  dih1dimatlem0  42143  dihglblem6  42155  dochexmidlem4  42278  mapdpglem32  42520  mapdh8ad  42594  mapdh9aOLDN  42605  hdmap11lem2  42657  hdmap14lem6  42688  frlmfzowrdb  43319  mzpmfp  43519  mzpsubst  43520  pellex  43603  pellfundex  43654  pellfund14gap  43655  qirropth  43676  rmxypos  43715  congmul  43735  congsub  43738  mzpcong  43740  coprmdvdsb  43753  jm2.15nn0  43771  jm2.16nn0  43772  rpnnen3lem  43799  idomsubgmo  43961  relexp01min  44480  mullimc  46373  islptre  46376  mullimcf  46380  addlimc  46403  0ellimcdiv  46404  limsupre3lem  46487  limsupre3uzlem  46490  fourierdlem48  46909  fourierdlem80  46941  opnvonmbllem2  47388  ovolval5lem3  47409  ovnovollem3  47413  difltmodne  48126  isubgr3stgrlem1  48772  grlimedgclnbgr  48801  mapprop  49167  lincfsuppcl  49234  lindslinindimp2lem3  49281  itsclc0lem1  49577  itsclc0lem2  49578  itschlc0yqe  49581  itsclc0xyqsolr  49590  swapffunc  50101  fucofunc  50178  fucoppc  50229