Theorem simp3r 1090

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl3r  1117  simpr3r  1123  simp13r  1177  simp23r  1183  simp33r  1189  f1oiso2  6602  tfisi  7058  tfrlem5  7476  omeulem1  7662  omeulem2  7663  elfiun  8336  isfin2-2  9141  addid2  10219  mulcan  10664  mulcan2  10665  divass  10703  divdir  10710  div11  10713  ltdiv1  10887  ltmuldiv  10896  lediv2  10913  xaddass2  12080  xlt2add  12090  expaddz  12904  expmulz  12906  resqrex  13991  resqrtcl  13994  o1add  14344  o1mul  14345  o1sub  14346  dvdsgcd  15261  rpexp12i  15434  pythagtriplem4  15524  pythagtriplem11  15530  pythagtriplem13  15532  pcpremul  15548  pceu  15551  pcqmul  15558  pcqdiv  15562  f1ocpbllem  16184  funcoppc  16535  funcres  16556  catcisolem  16756  1stfcl  16837  2ndfcl  16838  prfcl  16843  evlfcl  16862  curf1cl  16868  curfcl  16872  hofcl  16899  latjlej12  17067  latmlem12  17083  latj4  17101  latj4rot  17102  symgsssg  17887  symgfisg  17888  odcong  17968  cmn4  18212  ablsub4  18218  abladdsub4  18219  lsm4  18263  abvdom  18838  abvtrivd  18840  lspsolvlem  19142  lbsextlem2  19159  lidlsubcl  19216  frlmbas3  20115  matinvgcell  20241  matmulcell  20251  ma1repveval  20377  mdetunilem3  20420  mdetuni0  20427  mdetmul  20429  hausflimlem  21783  psmetlecl  22120  xmetlecl  22151  prdsxmetlem  22173  xblcntrps  22215  xblcntr  22216  bndth  22757  cph2ass  23013  iscau3  23076  dvres2  23676  coemullem  24006  vieta1  24067  aalioulem4  24090  cxpcn3lem  24488  angcan  24532  divsqrtsumlem  24706  dchrmusumlema  25182  dchrvmasumlema  25189  dchrisum0lema  25203  logdivsum  25222  padicabv  25319  ax5seglem3  25811  ax5seglem6  25814  axpasch  25821  axeuclid  25843  axcontlem4  25847  axcontlem8  25851  trlsonistrl  26605  pthonispth  26642  spthonisspth  26646  wspthneq1eq2  26745  frgr2wwlkeqm  27195  adjlnop  28945  xreceu  29630  orngmul  29803  rhmdvd  29821  measvunilem  30275  measvuni  30277  bnj1128  31058  cgrcomim  32096  cgrcoml  32103  cgrcomr  32104  cgrdegen  32111  segconeu  32118  btwnintr  32126  btwnexch3  32127  btwnouttr2  32129  btwnouttr  32131  btwnexch  32132  ifscgr  32151  lineext  32183  linecgr  32188  lineid  32190  idinside  32191  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem14  32207  btwnconn2  32209  btwnconn3  32210  midofsegid  32211  btwnoutside  32232  outsideoftr  32236  lineunray  32254  lineelsb2  32255  itg2addnclem  33461  cnres2  33562  heibor  33620  lsmcv2  34316  lcvat  34317  lcvexchlem4  34324  lcvexchlem5  34325  lfladd  34353  lflsub  34354  lflmul  34355  lshpkrlem4  34400  latm4  34520  omlmod1i2N  34547  cvlsupr7  34635  cvlsupr8  34636  hlatj4  34660  hlrelat3  34698  cvrval3  34699  atcvrj1  34717  atlelt  34724  2atlt  34725  2atjm  34731  3noncolr2  34735  athgt  34742  3dimlem2  34745  3dimlem4OLDN  34751  1cvratex  34759  ps-1  34763  ps-2  34764  hlatexch3N  34766  llnle  34804  atcvrlln2  34805  atcvrlln  34806  lplni2  34823  lplnle  34826  lplnnle2at  34827  lplnnlelln  34829  llncvrlpln2  34843  2llnmeqat  34857  lvolnle3at  34868  lvolnlelln  34870  4atlem0ae  34880  lneq2at  35064  lnjatN  35066  lncvrat  35068  2lnat  35070  elpaddri  35088  paddasslem2  35107  padd4N  35126  hlmod1i  35142  llnexchb2  35155  dalawlem2  35158  pclfinN  35186  pexmidlem4N  35259  pl42lem1N  35265  lhp2lt  35287  lhpexle1  35294  lhpexle2lem  35295  lhpj1  35308  lhpmcvr5N  35313  lhp2at0  35318  lhp2at0nle  35321  lhple  35328  lhpat  35329  lhpat4N  35330  4atexlemnslpq  35342  4atexlem7  35361  ltrn11  35412  ltrnle  35415  ltrnm  35417  ltrnj  35418  ltrncvr  35419  ltrnel  35425  ltrncnvel  35428  ltrncnv  35432  ltrnmwOLD  35438  trlat  35456  trl0  35457  trlnidat  35460  trlnid  35466  ltrnatlw  35470  trlne  35472  trlval4  35475  cdlemc5  35482  cdlemd2  35486  cdlemd7  35491  cdlemd8  35492  cdlemd9  35493  cdleme0c  35500  cdleme0e  35504  cdleme0fN  35505  cdleme3g  35521  cdleme3h  35522  cdleme5  35527  cdleme11c  35548  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme0nex  35577  cdleme18a  35578  cdleme22gb  35581  cdleme20zN  35588  cdleme20yOLD  35590  cdleme20c  35599  cdleme20k  35607  cdleme21a  35613  cdleme21b  35614  cdleme21c  35615  cdleme21ct  35617  cdleme21h  35622  cdleme22d  35631  cdleme22f  35634  cdleme26ee  35648  cdleme30a  35666  cdlemefs45eN  35719  cdleme36a  35748  cdleme36m  35749  cdleme39a  35753  cdleme42b  35766  cdleme43dN  35780  cdlemeg47rv2  35798  cdlemeg46sfg  35808  cdlemeg46rjgN  35810  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemeg46gfv  35818  cdleme48d  35823  cdleme50ltrn  35845  cdlemf1  35849  cdlemf  35851  cdlemg2dN  35878  cdlemg2fvlem  35882  cdlemg2l  35891  cdlemg7fvbwN  35895  cdlemg7aN  35913  cdlemg10c  35927  cdlemg17a  35949  cdlemg17dALTN  35952  cdlemg18a  35966  cdlemg18b  35967  cdlemg31b0a  35983  cdlemg31a  35985  cdlemg31b  35986  ltrnco  36007  cdlemg48  36025  tgrpov  36036  tendoco2  36056  tendoplco2  36067  cdlemh1  36103  cdlemk1  36119  cdlemk26b-3  36193  cdlemk27-3  36195  cdlemk28-3  36196  cdlemk34  36198  cdlemkfid1N  36209  cdlemkid3N  36221  cdlemkid4  36222  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk51  36241  tendospcanN  36312  cdlemm10N  36407  dicvaddcl  36479  dicvscacl  36480  cdlemn6  36491  dihvalcq2  36536  dihord6b  36549  dihord5apre  36551  dihglbcpreN  36589  dihjatc1  36600  dihmeetlem20N  36615  dih1dimatlem0  36617  dihglblem6  36629  dochexmidlem4  36752  mapdpglem32  36994  mapdh8ad  37068  mapdh9aOLDN  37080  hdmap11lem2  37134  hdmap14lem6  37165  mzpmfp  37310  mzpsubst  37311  pellex  37399  pellfundex  37450  pellfund14gap  37451  qirropth  37473  rmxypos  37514  congmul  37534  congsub  37537  mzpcong  37539  coprmdvdsb  37552  jm2.15nn0  37570  jm2.16nn0  37571  rpnnen3lem  37598  idomsubgmo  37776  relexp01min  38005  mullimc  39848  islptre  39851  mullimcf  39855  addlimc  39880  0ellimcdiv  39881  limsupre3lem  39964  limsupre3uzlem  39967  fourierdlem48  40371  fourierdlem80  40403  opnvonmbllem2  40847  ovolval5lem3  40868  ovnovollem3  40872  lincfsuppcl  42202  lindslinindimp2lem3  42249